| Age | Commit message (Collapse) | Author |
|---|
|
Deactivate plugins of the datatype package except for the size plugin in order
to keep processing time reasonable. This is currently only needed for the big
AST datatypes, so we just patch this using a sed command.
|
|
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.
|
|
|
|
Makefile which is useful because ocaml generation currently produces some spurious warnings due to running type checker between rewritings.
|
|
|
|
|
