equal
deleted
inserted
replaced
14 text {* For every type that is to be stored in a state space, an |
14 text {* For every type that is to be stored in a state space, an |
15 instance of this locale is imported in order convert the abstract and |
15 instance of this locale is imported in order convert the abstract and |
16 concrete values.*} |
16 concrete values.*} |
17 |
17 |
18 |
18 |
19 class_locale project_inject = |
19 locale project_inject = |
20 fixes project :: "'value \<Rightarrow> 'a" |
20 fixes project :: "'value \<Rightarrow> 'a" |
21 and "inject":: "'a \<Rightarrow> 'value" |
21 and "inject":: "'a \<Rightarrow> 'value" |
22 assumes project_inject_cancel [statefun_simp]: "project (inject x) = x" |
22 assumes project_inject_cancel [statefun_simp]: "project (inject x) = x" |
23 |
23 |
24 lemma (in project_inject) |
24 lemma (in project_inject) |