diff options
| author | Thomas Bauereiss | 2018-01-30 18:15:29 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-01-31 12:49:20 +0000 |
| commit | 3cad2ad60f5f5f05ef94ba38590539939d3ccda0 (patch) | |
| tree | aa58990cbecf5a0367990039321c0d7672dbddce /src/pretty_print_lem.ml | |
| parent | 0beb4619c72f2e1cc2123e278c1ed7744e350899 (diff) | |
Split base definitions of Lem monads and further built-ins (e.g. loop combinators)
Add Isabelle-specific theories imported directly after monad definitions, but
before other combinators. These theories contain lemmas that tell the function
package how to deal with monadic binds in function definitions.
Diffstat (limited to 'src/pretty_print_lem.ml')
| -rw-r--r-- | src/pretty_print_lem.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 48825540..5d127f6d 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -1495,15 +1495,15 @@ let pp_defs_lem (types_file,types_modules) (defs_file,defs_modules) d top_line = if !opt_sequential then concat [regstate_def; hardline; hardline; - string ("type MR 'a 'r = State.MR regstate 'a 'r " ^ exc_typ); hardline; - string ("type M 'a = State.M regstate 'a " ^ exc_typ); hardline; + string ("type MR 'a 'r = State_monad.MR regstate 'a 'r " ^ exc_typ); hardline; + string ("type M 'a = State_monad.M regstate 'a " ^ exc_typ); hardline; hardline; register_refs ] else concat [ - string ("type MR 'a 'r = Prompt.MR 'a 'r " ^ exc_typ); hardline; - string ("type M 'a = Prompt.M 'a " ^ exc_typ); hardline + string ("type MR 'a 'r = Prompt_monad.MR 'a 'r " ^ exc_typ); hardline; + string ("type M 'a = Prompt_monad.M 'a " ^ exc_typ); hardline ] ]); (print defs_file) |