diff options
| author | Thomas Bauereiss | 2018-02-23 19:38:40 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-02-26 13:30:21 +0000 |
| commit | 30ba876d4c465d9a6cf2eba4eb1ac4c3dbc7ed22 (patch) | |
| tree | f08e199bb2cc932928296ba2fcdb5bd50d1f7d75 /src/pattern_completeness.ml | |
| parent | f100cf44857926030361ef66cff795169c29fdbc (diff) | |
Add/generate Isabelle lemmas about the monad lifting
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.
Diffstat (limited to 'src/pattern_completeness.ml')
0 files changed, 0 insertions, 0 deletions