src/HOL/ex/Reflection.thy
author wenzelm
Thu Aug 03 15:03:05 2006 +0200 (2006-08-03)
changeset 20319 a8761e8568de
child 20374 01b711328990
permissions -rw-r--r--
Generic reflection and reification (by Amine Chaieb).
     1 (*
     2     ID:         $Id$
     3     Author:     Amine Chaieb, TU Muenchen
     4 *)
     5 
     6 header {* Generic reflection and reification *}
     7 
     8 theory Reflection
     9 imports Main
    10 uses "reflection.ML"
    11 begin
    12 
    13 method_setup reify = {*
    14   fn src =>
    15     Method.syntax (Attrib.thms --
    16       Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
    17   (fn (ctxt, (eqs,to)) => Method.SIMPLE_METHOD' HEADGOAL (Reflection.genreify_tac ctxt eqs to))
    18 *} "partial automatic reification"
    19 
    20 method_setup reflection = {*
    21   fn src =>
    22     Method.syntax (Attrib.thms --
    23       Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
    24   (fn (ctxt, (ths,to)) => Method.SIMPLE_METHOD' HEADGOAL (Reflection.reflection_tac ctxt ths to))
    25 *} "reflection method"
    26 
    27 end