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;
haftmann@29650
     1
(*  Title:      HOL/Library/reflection_data.ML
chaieb@23545
     2
    Author:     Amine Chaieb, TU Muenchen
chaieb@23545
     3
wenzelm@24045
     4
Data for the reification and reflection methods.
chaieb@23545
     5
*)
chaieb@23545
     6
chaieb@23545
     7
signature REIFY_DATA =
chaieb@23545
     8
sig
haftmann@29650
     9
  val get: Proof.context -> thm list * thm list
haftmann@29650
    10
  val add: attribute
chaieb@23606
    11
  val del: attribute
haftmann@29650
    12
  val radd: attribute
haftmann@29650
    13
  val rdel: attribute
chaieb@23545
    14
  val setup: theory -> theory
chaieb@23545
    15
end;
chaieb@23545
    16
chaieb@23545
    17
structure Reify_Data : REIFY_DATA =
chaieb@23545
    18
struct
chaieb@23545
    19
chaieb@23545
    20
structure Data = GenericDataFun
wenzelm@24045
    21
(
haftmann@29650
    22
  type T = thm list * thm list;
haftmann@29650
    23
  val empty = ([], []);
haftmann@29650
    24
  val extend = I;
haftmann@29650
    25
  fun merge _ = pairself Thm.merge_thms;
wenzelm@24045
    26
);
chaieb@23545
    27
chaieb@23545
    28
val get = Data.get o Context.Proof;
chaieb@23545
    29
haftmann@29650
    30
val add = Thm.declaration_attribute (Data.map o apfst o Thm.add_thm);
haftmann@29650
    31
val del = Thm.declaration_attribute (Data.map o apfst o Thm.del_thm);
haftmann@29650
    32
val radd = Thm.declaration_attribute (Data.map o apsnd o Thm.add_thm);
haftmann@29650
    33
val rdel = Thm.declaration_attribute (Data.map o apsnd o Thm.del_thm);
chaieb@23545
    34
wenzelm@30528
    35
val setup =
wenzelm@30528
    36
  Attrib.setup @{binding reify} (Attrib.add_del add del) "reify data" #>
wenzelm@30528
    37
  Attrib.setup @{binding reflection} (Attrib.add_del radd rdel) "reflection data";
chaieb@23545
    38
chaieb@23545
    39
end;