35 val print_qconstinfo: Proof.context -> unit |
35 val print_qconstinfo: Proof.context -> unit |
36 |
36 |
37 val equiv_rules_get: Proof.context -> thm list |
37 val equiv_rules_get: Proof.context -> thm list |
38 val equiv_rules_add: attribute |
38 val equiv_rules_add: attribute |
39 val rsp_rules_get: Proof.context -> thm list |
39 val rsp_rules_get: Proof.context -> thm list |
|
40 val rsp_rules_add: attribute |
40 val prs_rules_get: Proof.context -> thm list |
41 val prs_rules_get: Proof.context -> thm list |
|
42 val prs_rules_add: attribute |
41 val id_simps_get: Proof.context -> thm list |
43 val id_simps_get: Proof.context -> thm list |
42 val quotient_rules_get: Proof.context -> thm list |
44 val quotient_rules_get: Proof.context -> thm list |
43 val quotient_rules_add: attribute |
45 val quotient_rules_add: attribute |
44 end; |
46 end; |
45 |
47 |
239 structure RspRules = Named_Thms |
241 structure RspRules = Named_Thms |
240 (val name = "quot_respect" |
242 (val name = "quot_respect" |
241 val description = "Respectfulness theorems.") |
243 val description = "Respectfulness theorems.") |
242 |
244 |
243 val rsp_rules_get = RspRules.get |
245 val rsp_rules_get = RspRules.get |
|
246 val rsp_rules_add = RspRules.add |
244 |
247 |
245 (* preservation theorems *) |
248 (* preservation theorems *) |
246 structure PrsRules = Named_Thms |
249 structure PrsRules = Named_Thms |
247 (val name = "quot_preserve" |
250 (val name = "quot_preserve" |
248 val description = "Preservation theorems.") |
251 val description = "Preservation theorems.") |
249 |
252 |
250 val prs_rules_get = PrsRules.get |
253 val prs_rules_get = PrsRules.get |
|
254 val prs_rules_add = PrsRules.add |
251 |
255 |
252 (* id simplification theorems *) |
256 (* id simplification theorems *) |
253 structure IdSimps = Named_Thms |
257 structure IdSimps = Named_Thms |
254 (val name = "id_simps" |
258 (val name = "id_simps" |
255 val description = "Identity simp rules for maps.") |
259 val description = "Identity simp rules for maps.") |