src/HOL/Library/Reflection.thy
changeset 45966 03ce2b2a29a2
parent 42814 5af15f1e2ef6
child 46510 696f3fec3f83
     1.1 --- a/src/HOL/Library/Reflection.thy	Sat Dec 24 15:53:09 2011 +0100
     1.2 +++ b/src/HOL/Library/Reflection.thy	Sat Dec 24 15:53:09 2011 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4  setup {* Reify_Data.setup *}
     1.5  
     1.6  lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g"
     1.7 -  by (blast intro: ext)
     1.8 +  by blast
     1.9  
    1.10  use "reflection.ML"
    1.11