equal
deleted
inserted
replaced
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 |
34 |
35 functor Named_Thms_Ext (val name: string val description: string val filter: thm -> thm): NAMED_THMS = |
35 |
|
36 functor Filtered_Named_Thms (val name: string val description: string val filter: thm -> thm): NAMED_THMS = |
36 struct |
37 struct |
37 |
38 |
38 structure Data = Generic_Data |
39 structure Data = Generic_Data |
39 ( |
40 ( type T = thm Item_Net.T; |
40 type T = thm Item_Net.T; |
|
41 val empty = Thm.full_rules; |
41 val empty = Thm.full_rules; |
42 val extend = I; |
42 val extend = I; |
43 val merge = Item_Net.merge; |
43 val merge = Item_Net.merge); |
44 ); |
|
45 |
44 |
46 val content = Item_Net.content o Data.get; |
45 val content = Item_Net.content o Data.get; |
47 val get = content o Context.Proof; |
46 val get = content o Context.Proof; |
48 |
47 |
49 val add_thm = Data.map o Item_Net.update o filter; |
48 val add_thm = Data.map o Item_Net.update o filter; |
242 |
241 |
243 val equiv_rules_get = EquivRules.get |
242 val equiv_rules_get = EquivRules.get |
244 val equiv_rules_add = EquivRules.add |
243 val equiv_rules_add = EquivRules.add |
245 |
244 |
246 (* respectfulness theorems *) |
245 (* respectfulness theorems *) |
247 structure RspRules = Named_Thms_Ext |
246 structure RspRules = Filtered_Named_Thms |
248 (val name = "quot_respect" |
247 (val name = "quot_respect" |
249 val description = "Respectfulness theorems." |
248 val description = "Respectfulness theorems." |
250 val filter = fn x => x) |
249 val filter = I) |
251 |
250 |
252 val rsp_rules_get = RspRules.get |
251 val rsp_rules_get = RspRules.get |
253 |
252 |
254 (* preservation theorems *) |
253 (* preservation theorems *) |
255 structure PrsRules = Named_Thms |
254 structure PrsRules = Named_Thms |
280 RspRules.setup #> |
279 RspRules.setup #> |
281 PrsRules.setup #> |
280 PrsRules.setup #> |
282 IdSimps.setup #> |
281 IdSimps.setup #> |
283 QuotientRules.setup)) |
282 QuotientRules.setup)) |
284 |
283 |
285 |
|
286 (* setup of the printing commands *) |
284 (* setup of the printing commands *) |
287 |
285 |
288 fun improper_command (pp_fn, cmd_name, descr_str) = |
286 fun improper_command (pp_fn, cmd_name, descr_str) = |
289 OuterSyntax.improper_command cmd_name descr_str |
287 OuterSyntax.improper_command cmd_name descr_str |
290 OuterKeyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of))) |
288 OuterKeyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of))) |