| changeset 51378 | 502f6a53519b |
| parent 51301 | 6822aa82aafa |
| child 51542 | 738598beeb26 |
--- a/src/HOL/Library/Phantom_Type.thy Fri Mar 08 13:21:52 2013 +0100 +++ b/src/HOL/Library/Phantom_Type.thy Fri Mar 08 13:21:55 2013 +0100 @@ -17,8 +17,6 @@ lemma type_definition_phantom': "type_definition of_phantom phantom UNIV" by(unfold_locales) simp_all -setup_lifting (no_code) type_definition_phantom' - lemma phantom_comp_of_phantom [simp]: "phantom \<circ> of_phantom = id" and of_phantom_comp_phantom [simp]: "of_phantom \<circ> phantom = id" by(simp_all add: o_def id_def)