author | haftmann |
Wed, 28 Jan 2009 11:04:10 +0100 | |
changeset 29650 | cc3958d31b1d |
parent 25979 | src/HOL/ex/reflection_data.ML@3297781f8141 |
child 30528 | 7173bf123335 |
permissions | -rw-r--r-- |
29650 | 1 |
(* Title: HOL/Library/reflection_data.ML |
23545 | 2 |
Author: Amine Chaieb, TU Muenchen |
3 |
||
24045
bead02a55952
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23647
diff
changeset
|
4 |
Data for the reification and reflection methods. |
23545 | 5 |
*) |
6 |
||
7 |
signature REIFY_DATA = |
|
8 |
sig |
|
29650 | 9 |
val get: Proof.context -> thm list * thm list |
10 |
val add: attribute |
|
23606 | 11 |
val del: attribute |
29650 | 12 |
val radd: attribute |
13 |
val rdel: attribute |
|
23545 | 14 |
val setup: theory -> theory |
15 |
end; |
|
16 |
||
17 |
structure Reify_Data : REIFY_DATA = |
|
18 |
struct |
|
19 |
||
20 |
structure Data = GenericDataFun |
|
24045
bead02a55952
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23647
diff
changeset
|
21 |
( |
29650 | 22 |
type T = thm list * thm list; |
23 |
val empty = ([], []); |
|
24 |
val extend = I; |
|
25 |
fun merge _ = pairself Thm.merge_thms; |
|
24045
bead02a55952
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23647
diff
changeset
|
26 |
); |
23545 | 27 |
|
28 |
val get = Data.get o Context.Proof; |
|
29 |
||
29650 | 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); |
|
23545 | 34 |
|
29650 | 35 |
val setup = Attrib.add_attributes |
36 |
[("reify", Attrib.add_del_args add del, "Reify data"), |
|
37 |
("reflection", Attrib.add_del_args radd rdel, "Reflection data")]; |
|
23545 | 38 |
|
39 |
end; |