Rebase state monad onto prompt monad

Generate only one Lem model based on the prompt monad (instead of two models
with different monads), and add a lifting from prompt to state monad.  Add some
Isabelle lemmas about the monad lifting.

Also drop the "_embed" and "_sequential" suffixes from names of generated
files.

1 files changed, 1 insertions, 1 deletions

diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 34e4bd98..3d55843e 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -608,7 +608,7 @@ type register =
 
 type register_ref 'regstate 'regval 'a =
   <| name : string;
-     is_inc : bool;
+     (*is_inc : bool;*)
      read_from : 'regstate -> 'a;
      write_to : 'regstate -> 'a -> 'regstate;
      of_regval : 'regval -> maybe 'a;