author | kuncar |
Fri, 08 Mar 2013 13:21:55 +0100 | |
changeset 51378 | 502f6a53519b |
parent 51377 | 7da251a6c16e |
child 51379 | 6dd83e007f56 |
--- 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)