src/HOL/Library/reify_data.ML
author wenzelm
Sun Mar 15 15:59:44 2009 +0100 (2009-03-15)
changeset 30528 7173bf123335
parent 29650 cc3958d31b1d
child 33518 24563731b9b2
permissions -rw-r--r--
simplified attribute setup;
     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 =
    36   Attrib.setup @{binding reify} (Attrib.add_del add del) "reify data" #>
    37   Attrib.setup @{binding reflection} (Attrib.add_del radd rdel) "reflection data";
    38 
    39 end;