equal
deleted
inserted
replaced
29 val prs_rules_get: Proof.context -> thm list |
29 val prs_rules_get: Proof.context -> thm list |
30 val id_simps_get: Proof.context -> thm list |
30 val id_simps_get: Proof.context -> thm list |
31 val quotient_rules_get: Proof.context -> thm list |
31 val quotient_rules_get: Proof.context -> thm list |
32 val quotient_rules_add: attribute |
32 val quotient_rules_add: attribute |
33 end; |
33 end; |
|
34 |
|
35 functor Named_Thms_Ext (val name: string val description: string val filter: thm -> thm): NAMED_THMS = |
|
36 struct |
|
37 |
|
38 structure Data = Generic_Data |
|
39 ( |
|
40 type T = thm Item_Net.T; |
|
41 val empty = Thm.full_rules; |
|
42 val extend = I; |
|
43 val merge = Item_Net.merge; |
|
44 ); |
|
45 |
|
46 val content = Item_Net.content o Data.get; |
|
47 val get = content o Context.Proof; |
|
48 |
|
49 val add_thm = Data.map o Item_Net.update o filter; |
|
50 val del_thm = Data.map o Item_Net.remove; |
|
51 |
|
52 val add = Thm.declaration_attribute add_thm; |
|
53 val del = Thm.declaration_attribute del_thm; |
|
54 |
|
55 val setup = |
|
56 Attrib.setup (Binding.name name) (Attrib.add_del add del) ("declaration of " ^ description) #> |
|
57 PureThy.add_thms_dynamic (Binding.name name, content); |
|
58 |
|
59 end; |
|
60 |
|
61 |
34 |
62 |
35 structure Quotient_Info: QUOTIENT_INFO = |
63 structure Quotient_Info: QUOTIENT_INFO = |
36 struct |
64 struct |
37 |
65 |
38 exception NotFound |
66 exception NotFound |
214 |
242 |
215 val equiv_rules_get = EquivRules.get |
243 val equiv_rules_get = EquivRules.get |
216 val equiv_rules_add = EquivRules.add |
244 val equiv_rules_add = EquivRules.add |
217 |
245 |
218 (* respectfulness theorems *) |
246 (* respectfulness theorems *) |
219 structure RspRules = Named_Thms |
247 structure RspRules = Named_Thms_Ext |
220 (val name = "quot_respect" |
248 (val name = "quot_respect" |
221 val description = "Respectfulness theorems.") |
249 val description = "Respectfulness theorems." |
|
250 val filter = fn x => x) |
222 |
251 |
223 val rsp_rules_get = RspRules.get |
252 val rsp_rules_get = RspRules.get |
224 |
253 |
225 (* preservation theorems *) |
254 (* preservation theorems *) |
226 structure PrsRules = Named_Thms |
255 structure PrsRules = Named_Thms |