equal
deleted
inserted
replaced
40 val prs_rules_get: Proof.context -> thm list |
40 val prs_rules_get: Proof.context -> thm list |
41 val id_simps_get: Proof.context -> thm list |
41 val id_simps_get: Proof.context -> thm list |
42 val quotient_rules_get: Proof.context -> thm list |
42 val quotient_rules_get: Proof.context -> thm list |
43 val quotient_rules_add: attribute |
43 val quotient_rules_add: attribute |
44 end; |
44 end; |
45 |
|
46 |
|
47 functor Filtered_Named_Thms (val name: string val description: string val filter: thm -> thm): NAMED_THMS = |
|
48 struct |
|
49 |
|
50 structure Data = Generic_Data |
|
51 ( type T = thm Item_Net.T; |
|
52 val empty = Thm.full_rules; |
|
53 val extend = I; |
|
54 val merge = Item_Net.merge); |
|
55 |
|
56 val content = Item_Net.content o Data.get; |
|
57 val get = content o Context.Proof; |
|
58 |
|
59 val add_thm = Data.map o Item_Net.update o filter; |
|
60 val del_thm = Data.map o Item_Net.remove; |
|
61 |
|
62 val add = Thm.declaration_attribute add_thm; |
|
63 val del = Thm.declaration_attribute del_thm; |
|
64 |
|
65 val setup = |
|
66 Attrib.setup (Binding.name name) (Attrib.add_del add del) ("declaration of " ^ description) #> |
|
67 PureThy.add_thms_dynamic (Binding.name name, content); |
|
68 |
|
69 end; |
|
70 |
|
71 |
45 |
72 |
46 |
73 structure Quotient_Info: QUOTIENT_INFO = |
47 structure Quotient_Info: QUOTIENT_INFO = |
74 struct |
48 struct |
75 |
49 |
260 |
234 |
261 val equiv_rules_get = EquivRules.get |
235 val equiv_rules_get = EquivRules.get |
262 val equiv_rules_add = EquivRules.add |
236 val equiv_rules_add = EquivRules.add |
263 |
237 |
264 (* respectfulness theorems *) |
238 (* respectfulness theorems *) |
265 structure RspRules = Filtered_Named_Thms |
239 structure RspRules = Named_Thms |
266 (val name = "quot_respect" |
240 (val name = "quot_respect" |
267 val description = "Respectfulness theorems." |
241 val description = "Respectfulness theorems.") |
268 val filter = I) |
|
269 |
242 |
270 val rsp_rules_get = RspRules.get |
243 val rsp_rules_get = RspRules.get |
271 |
244 |
272 (* preservation theorems *) |
245 (* preservation theorems *) |
273 structure PrsRules = Named_Thms |
246 structure PrsRules = Named_Thms |