src/HOL/Library/reify_data.ML
author huffman
Thu Jun 11 09:03:24 2009 -0700 (2009-06-11)
changeset 31563 ded2364d14d4
parent 30528 7173bf123335
child 33518 24563731b9b2
permissions -rw-r--r--
cleaned up some proofs
     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;