author | hoelzl |
Thu, 17 Jan 2013 11:59:12 +0100 | |
changeset 50936 | b28f258ebc1a |
parent 37744 | 3daaf23b9ab4 |
permissions | -rw-r--r-- |
37744 | 1 |
(* Title: HOL/Library/reify_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 |
||
33518 | 20 |
structure Data = Generic_Data |
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; |
|
33518 | 25 |
fun merge ((ths1, rths1), (ths2, rths2)) = |
26 |
(Thm.merge_thms (ths1, ths2), Thm.merge_thms (rths1, rths2)); |
|
24045
bead02a55952
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23647
diff
changeset
|
27 |
); |
23545 | 28 |
|
29 |
val get = Data.get o Context.Proof; |
|
30 |
||
29650 | 31 |
val add = Thm.declaration_attribute (Data.map o apfst o Thm.add_thm); |
32 |
val del = Thm.declaration_attribute (Data.map o apfst o Thm.del_thm); |
|
33 |
val radd = Thm.declaration_attribute (Data.map o apsnd o Thm.add_thm); |
|
34 |
val rdel = Thm.declaration_attribute (Data.map o apsnd o Thm.del_thm); |
|
23545 | 35 |
|
30528 | 36 |
val setup = |
37 |
Attrib.setup @{binding reify} (Attrib.add_del add del) "reify data" #> |
|
38 |
Attrib.setup @{binding reflection} (Attrib.add_del radd rdel) "reflection data"; |
|
23545 | 39 |
|
40 |
end; |