sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2018-02-26	Add/generate Isabelle lemmas about the monad lifting	Thomas Bauereiss
	Architecture-specific lemmas about concrete registers and types are generated and written to a file <prefix>_lemmas.thy, generic lemmas are in the theories *_extras.thy in lib/isabelle. In particular, State_extras contains simplification lemmas about the lifting from prompt to state monad.
2018-02-15	Rebase state monad onto prompt monad	Thomas Bauereiss
	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.