src/HOL/ex/Reflection.thy
changeset 23546 c8a1bd9585a0
parent 22199 b617ddd200eb
child 23607 6a8fb529b542
     1.1 --- a/src/HOL/ex/Reflection.thy	Tue Jul 03 17:49:53 2007 +0200
     1.2 +++ b/src/HOL/ex/Reflection.thy	Tue Jul 03 17:49:55 2007 +0200
     1.3 @@ -7,26 +7,30 @@
     1.4  
     1.5  theory Reflection
     1.6  imports Main
     1.7 -  uses ("reflection.ML")
     1.8 +  uses "reflection_data.ML" ("reflection.ML")
     1.9  begin
    1.10  
    1.11 +setup {* Reify_Data.setup*}
    1.12 +
    1.13 +
    1.14  lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g"
    1.15    by (blast intro: ext)
    1.16  
    1.17  use "reflection.ML"
    1.18 +ML{* Reify_Data.get @{context}*}
    1.19  
    1.20  method_setup reify = {*
    1.21    fn src =>
    1.22      Method.syntax (Attrib.thms --
    1.23        Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
    1.24 -  (fn ((eqs, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt eqs to))
    1.25 +  (fn ((eqs, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ Reify_Data.get ctxt) to))
    1.26  *} "partial automatic reification"
    1.27  
    1.28  method_setup reflection = {*
    1.29    fn src =>
    1.30      Method.syntax (Attrib.thms --
    1.31        Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
    1.32 -  (fn ((ths, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt ths to))
    1.33 +  (fn ((ths, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt (ths @ Reify_Data.get ctxt) to))
    1.34  *} "reflection method"
    1.35  
    1.36  end