src/HOL/Library/Reflection.thy
changeset 46510 696f3fec3f83
parent 45966 03ce2b2a29a2
child 46764 a65e18ceb1e3
     1.1 --- a/src/HOL/Library/Reflection.thy	Thu Feb 16 22:54:40 2012 +0100
     1.2 +++ b/src/HOL/Library/Reflection.thy	Thu Feb 16 23:07:01 2012 +0100
     1.3 @@ -11,9 +11,6 @@
     1.4  
     1.5  setup {* Reify_Data.setup *}
     1.6  
     1.7 -lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g"
     1.8 -  by blast
     1.9 -
    1.10  use "reflection.ML"
    1.11  
    1.12  method_setup reify = {*