diff options
| author | Thomas Bauereiss | 2018-05-18 16:57:50 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-05-18 20:11:24 +0100 |
| commit | e2aa34b0ba28d89eab9f845fe904d4fdebb17395 (patch) | |
| tree | 9c6876af33071cd5f298573d5963400cc7e81cdf /src | |
| parent | 1644cf140a58b53ebfaebd90559d5a449df9e270 (diff) | |
Make named theorem collections of state monad more fine-grained
Diffstat (limited to 'src')
| -rw-r--r-- | src/state.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/state.ml b/src/state.ml index ab63747c..112b4ee2 100644 --- a/src/state.ml +++ b/src/state.ml @@ -366,11 +366,11 @@ let generate_isa_lemmas mwords (Defs defs : tannot defs) = let id = remove_leading_underscores (string_of_id id) in let id' = remove_trailing_underscores id in separate_map hardline string [ - "lemma liftS_read_reg_" ^ id ^ "[simp]:"; + "lemma liftS_read_reg_" ^ id ^ "[liftState_simp]:"; " \"liftS (read_reg " ^ id ^ "_ref) = readS (" ^ id' ^ " \\<circ> regstate)\""; " by (auto simp: liftState_read_reg_readS register_defs)"; ""; - "lemma liftS_write_reg_" ^ id ^ "[simp]:"; + "lemma liftS_write_reg_" ^ id ^ "[liftState_simp]:"; " \"liftS (write_reg " ^ id ^ "_ref v) = updateS (regstate_update (" ^ id' ^ "_update (\\<lambda>_. v)))\""; " by (auto simp: liftState_write_reg_updateS register_defs)" ] |