src/HOL/Library/reify_data.ML
author haftmann
Wed Jan 28 11:04:10 2009 +0100 (2009-01-28)
changeset 29650 cc3958d31b1d
parent 25979 src/HOL/ex/reflection_data.ML@3297781f8141
child 30528 7173bf123335
permissions -rw-r--r--
Reflection.thy now in HOL/Library
     1 (*  Title:      HOL/Library/reflection_data.ML
     2     Author:     Amine Chaieb, TU Muenchen
     3 
     4 Data for the reification and reflection methods.
     5 *)
     6 
     7 signature REIFY_DATA =
     8 sig
     9   val get: Proof.context -> thm list * thm list
    10   val add: attribute
    11   val del: attribute
    12   val radd: attribute
    13   val rdel: attribute
    14   val setup: theory -> theory
    15 end;
    16 
    17 structure Reify_Data : REIFY_DATA =
    18 struct
    19 
    20 structure Data = GenericDataFun
    21 (
    22   type T = thm list * thm list;
    23   val empty = ([], []);
    24   val extend = I;
    25   fun merge _ = pairself Thm.merge_thms;
    26 );
    27 
    28 val get = Data.get o Context.Proof;
    29 
    30 val add = Thm.declaration_attribute (Data.map o apfst o Thm.add_thm);
    31 val del = Thm.declaration_attribute (Data.map o apfst o Thm.del_thm);
    32 val radd = Thm.declaration_attribute (Data.map o apsnd o Thm.add_thm);
    33 val rdel = Thm.declaration_attribute (Data.map o apsnd o Thm.del_thm);
    34 
    35 val setup = Attrib.add_attributes
    36   [("reify", Attrib.add_del_args add del, "Reify data"),
    37    ("reflection", Attrib.add_del_args radd rdel, "Reflection data")];
    38 
    39 end;