diff options
Diffstat (limited to 'lib/isabelle')
| -rw-r--r-- | lib/isabelle/Makefile | 6 | ||||
| -rw-r--r-- | lib/isabelle/Prompt_monad_lemmas.thy (renamed from lib/isabelle/Prompt_monad_extras.thy) | 4 | ||||
| -rw-r--r-- | lib/isabelle/ROOT | 4 | ||||
| -rw-r--r-- | lib/isabelle/Sail_values_lemmas.thy (renamed from lib/isabelle/Sail_values_extras.thy) | 2 | ||||
| -rw-r--r-- | lib/isabelle/State_lemmas.thy (renamed from lib/isabelle/State_extras.thy) | 2 | ||||
| -rw-r--r-- | lib/isabelle/State_monad_lemmas.thy (renamed from lib/isabelle/State_monad_extras.thy) | 4 |
6 files changed, 11 insertions, 11 deletions
diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile index 1cff8f61..688dfa07 100644 --- a/lib/isabelle/Makefile +++ b/lib/isabelle/Makefile @@ -1,7 +1,7 @@ THYS = Sail_instr_kinds.thy Sail_values.thy Sail_operators.thy \ Sail_operators_mwords.thy Sail_operators_bitlists.thy \ State_monad.thy State.thy Prompt_monad.thy Prompt.thy -EXTRA_THYS = State_monad_extras.thy State_extras.thy Prompt_monad_extras.thy +EXTRA_THYS = State_monad_lemmas.thy State_lemmas.thy Prompt_monad_lemmas.thy .PHONY: all heap-img clean @@ -32,13 +32,13 @@ Sail_operators_bitlists.thy: ../../src/gen_lib/sail_operators_bitlists.lem Sail_ Prompt_monad.thy: ../../src/gen_lib/prompt_monad.lem Sail_values.thy lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $< -Prompt.thy: ../../src/gen_lib/prompt.lem Prompt_monad.thy Prompt_monad_extras.thy +Prompt.thy: ../../src/gen_lib/prompt.lem Prompt_monad.thy Prompt_monad_lemmas.thy lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $< State_monad.thy: ../../src/gen_lib/state_monad.lem Sail_values.thy lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $< -State.thy: ../../src/gen_lib/state.lem Prompt.thy State_monad.thy State_monad_extras.thy +State.thy: ../../src/gen_lib/state.lem Prompt.thy State_monad.thy State_monad_lemmas.thy lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $< clean: diff --git a/lib/isabelle/Prompt_monad_extras.thy b/lib/isabelle/Prompt_monad_lemmas.thy index 9d29f5a2..d2466764 100644 --- a/lib/isabelle/Prompt_monad_extras.thy +++ b/lib/isabelle/Prompt_monad_lemmas.thy @@ -1,7 +1,7 @@ -theory Prompt_monad_extras +theory Prompt_monad_lemmas imports Prompt_monad - Sail_values_extras + Sail_values_lemmas begin lemma All_bind_dom: "bind_dom (m, f)" diff --git a/lib/isabelle/ROOT b/lib/isabelle/ROOT index b07bc807..4c5079fe 100644 --- a/lib/isabelle/ROOT +++ b/lib/isabelle/ROOT @@ -1,9 +1,9 @@ session "Sail" = "LEM" + options [document = false] theories - Sail_values_extras + Sail_values_lemmas Prompt - State_extras + State_lemmas Sail_operators_mwords Sail_operators_bitlists diff --git a/lib/isabelle/Sail_values_extras.thy b/lib/isabelle/Sail_values_lemmas.thy index 66bcba48..2114d991 100644 --- a/lib/isabelle/Sail_values_extras.thy +++ b/lib/isabelle/Sail_values_lemmas.thy @@ -1,4 +1,4 @@ -theory Sail_values_extras +theory Sail_values_lemmas imports Sail_values begin diff --git a/lib/isabelle/State_extras.thy b/lib/isabelle/State_lemmas.thy index 924861b0..e230bd37 100644 --- a/lib/isabelle/State_extras.thy +++ b/lib/isabelle/State_lemmas.thy @@ -1,4 +1,4 @@ -theory State_extras +theory State_lemmas imports State begin diff --git a/lib/isabelle/State_monad_extras.thy b/lib/isabelle/State_monad_lemmas.thy index 406aec79..fe827c66 100644 --- a/lib/isabelle/State_monad_extras.thy +++ b/lib/isabelle/State_monad_lemmas.thy @@ -1,7 +1,7 @@ -theory State_monad_extras +theory State_monad_lemmas imports State_monad - Sail_values_extras + Sail_values_lemmas begin context |