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
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
haftmann@29650
    35
val setup = Attrib.add_attributes
haftmann@29650
    36
  [("reify", Attrib.add_del_args add del, "Reify data"),
haftmann@29650
    37
   ("reflection", Attrib.add_del_args radd rdel, "Reflection data")];
chaieb@23545
    38
chaieb@23545
    39
end;