equal
deleted
inserted
replaced
15 by(cases x) simp |
15 by(cases x) simp |
16 |
16 |
17 lemma type_definition_phantom': "type_definition of_phantom phantom UNIV" |
17 lemma type_definition_phantom': "type_definition of_phantom phantom UNIV" |
18 by(unfold_locales) simp_all |
18 by(unfold_locales) simp_all |
19 |
19 |
20 setup_lifting (no_code) type_definition_phantom' |
|
21 |
|
22 lemma phantom_comp_of_phantom [simp]: "phantom \<circ> of_phantom = id" |
20 lemma phantom_comp_of_phantom [simp]: "phantom \<circ> of_phantom = id" |
23 and of_phantom_comp_phantom [simp]: "of_phantom \<circ> phantom = id" |
21 and of_phantom_comp_phantom [simp]: "of_phantom \<circ> phantom = id" |
24 by(simp_all add: o_def id_def) |
22 by(simp_all add: o_def id_def) |
25 |
23 |
26 syntax "_Phantom" :: "type \<Rightarrow> logic" ("(1Phantom/(1'(_')))") |
24 syntax "_Phantom" :: "type \<Rightarrow> logic" ("(1Phantom/(1'(_')))") |