summaryrefslogtreecommitdiff
path: root/lib/isabelle/Sail_values_extras.thy
AgeCommit message (Collapse)Author
2018-02-26Rename some Isabelle theoriesThomas Bauereiss
The suffix _lemmas is more descriptive than _extras.
2018-02-26Add/generate Isabelle lemmas about the monad liftingThomas 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.