equal
deleted
inserted
replaced
1 (* Title: HOL/Library/reify_data.ML |
|
2 Author: Amine Chaieb, TU Muenchen |
|
3 |
|
4 Data for the reification and reflection methods. |
|
5 *) |
|
6 |
|
7 signature REIFY_DATA = |
|
8 sig |
|
9 val get: Proof.context -> thm list * thm list |
|
10 val add: attribute |
|
11 val del: attribute |
|
12 val radd: attribute |
|
13 val rdel: attribute |
|
14 val setup: theory -> theory |
|
15 end; |
|
16 |
|
17 structure Reify_Data : REIFY_DATA = |
|
18 struct |
|
19 |
|
20 structure Data = Generic_Data |
|
21 ( |
|
22 type T = thm list * thm list; |
|
23 val empty = ([], []); |
|
24 val extend = I; |
|
25 fun merge ((ths1, rths1), (ths2, rths2)) = |
|
26 (Thm.merge_thms (ths1, ths2), Thm.merge_thms (rths1, rths2)); |
|
27 ); |
|
28 |
|
29 val get = Data.get o Context.Proof; |
|
30 |
|
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); |
|
35 |
|
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"; |
|
39 |
|
40 end; |
|