Rename some Isabelle theories

The suffix _lemmas is more descriptive than _extras.

8 files changed, 13 insertions, 13 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
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 728014eb..bca09aa1 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -2,7 +2,7 @@ open import Pervasives_extra
 (*open import Sail_impl_base*)
 open import Sail_values
 open import Prompt_monad
-open import {isabelle} `Prompt_monad_extras`
+open import {isabelle} `Prompt_monad_lemmas`
 
 val iter_aux : forall 'rv 'a 'e. integer -> (integer -> 'a -> monad 'rv unit 'e) -> list 'a -> monad 'rv unit 'e
 let rec iter_aux i f xs = match xs with
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 1740174e..1366e605 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -4,7 +4,7 @@ open import Sail_values
 open import Prompt_monad
 open import Prompt
 open import State_monad
-open import {isabelle} `State_monad_extras`
+open import {isabelle} `State_monad_lemmas`
 
 (* State monad wrapper around prompt monad *)