author | haftmann |
Tue, 23 Jun 2009 14:24:58 +0200 | |
changeset 31776 | 151c3f5f28f9 |
parent 30528 | 7173bf123335 |
child 33518 | 24563731b9b2 |
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 |
|
30528 | 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"; |
|
23545 | 38 |
|
39 |
end; |