src/HOL/Library/reify_data.ML
changeset 29650 cc3958d31b1d
parent 25979 3297781f8141
child 30528 7173bf123335
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/reify_data.ML	Wed Jan 28 11:04:10 2009 +0100
     1.3 @@ -0,0 +1,39 @@
     1.4 +(*  Title:      HOL/Library/reflection_data.ML
     1.5 +    Author:     Amine Chaieb, TU Muenchen
     1.6 +
     1.7 +Data for the reification and reflection methods.
     1.8 +*)
     1.9 +
    1.10 +signature REIFY_DATA =
    1.11 +sig
    1.12 +  val get: Proof.context -> thm list * thm list
    1.13 +  val add: attribute
    1.14 +  val del: attribute
    1.15 +  val radd: attribute
    1.16 +  val rdel: attribute
    1.17 +  val setup: theory -> theory
    1.18 +end;
    1.19 +
    1.20 +structure Reify_Data : REIFY_DATA =
    1.21 +struct
    1.22 +
    1.23 +structure Data = GenericDataFun
    1.24 +(
    1.25 +  type T = thm list * thm list;
    1.26 +  val empty = ([], []);
    1.27 +  val extend = I;
    1.28 +  fun merge _ = pairself Thm.merge_thms;
    1.29 +);
    1.30 +
    1.31 +val get = Data.get o Context.Proof;
    1.32 +
    1.33 +val add = Thm.declaration_attribute (Data.map o apfst o Thm.add_thm);
    1.34 +val del = Thm.declaration_attribute (Data.map o apfst o Thm.del_thm);
    1.35 +val radd = Thm.declaration_attribute (Data.map o apsnd o Thm.add_thm);
    1.36 +val rdel = Thm.declaration_attribute (Data.map o apsnd o Thm.del_thm);
    1.37 +
    1.38 +val setup = Attrib.add_attributes
    1.39 +  [("reify", Attrib.add_del_args add del, "Reify data"),
    1.40 +   ("reflection", Attrib.add_del_args radd rdel, "Reflection data")];
    1.41 +
    1.42 +end;