src/HOL/ex/Reflection.thy
changeset 20374 01b711328990
parent 20319 a8761e8568de
child 21588 cd0dc678a205
     1.1 --- a/src/HOL/ex/Reflection.thy	Wed Aug 09 18:41:42 2006 +0200
     1.2 +++ b/src/HOL/ex/Reflection.thy	Mon Aug 14 11:13:50 2006 +0200
     1.3 @@ -7,9 +7,13 @@
     1.4  
     1.5  theory Reflection
     1.6  imports Main
     1.7 -uses "reflection.ML"
     1.8 +uses ("reflection.ML")
     1.9  begin
    1.10  
    1.11 +lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g"
    1.12 +  by (blast intro: ext)
    1.13 +use "reflection.ML"
    1.14 +
    1.15  method_setup reify = {*
    1.16    fn src =>
    1.17      Method.syntax (Attrib.thms --