| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-02-26 | Rename some Isabelle theories | Thomas Bauereiss | |
| The suffix _lemmas is more descriptive than _extras. | |||
| 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. | |||
