24 val print_qconstinfo: Proof.context -> unit |
24 val print_qconstinfo: Proof.context -> unit |
25 |
25 |
26 val equiv_rules_get: Proof.context -> thm list |
26 val equiv_rules_get: Proof.context -> thm list |
27 val equiv_rules_add: attribute |
27 val equiv_rules_add: attribute |
28 val rsp_rules_get: Proof.context -> thm list |
28 val rsp_rules_get: Proof.context -> thm list |
|
29 val prs_rules_get: Proof.context -> thm list |
29 val id_simps_get: Proof.context -> thm list |
30 val id_simps_get: Proof.context -> thm list |
30 val quotient_rules_get: Proof.context -> thm list |
31 val quotient_rules_get: Proof.context -> thm list |
31 val quotient_rules_add: attribute |
32 val quotient_rules_add: attribute |
32 end; |
33 end; |
33 |
34 |
178 (* FIXME/TODO: check the various lemmas conform *) |
179 (* FIXME/TODO: check the various lemmas conform *) |
179 (* with the required shape *) |
180 (* with the required shape *) |
180 |
181 |
181 (* equivalence relation theorems *) |
182 (* equivalence relation theorems *) |
182 structure EquivRules = Named_Thms |
183 structure EquivRules = Named_Thms |
183 (val name = "quotient_equiv" |
184 (val name = "quot_equiv" |
184 val description = "Equivalence relation theorems.") |
185 val description = "Equivalence relation theorems.") |
185 |
186 |
186 val equiv_rules_get = EquivRules.get |
187 val equiv_rules_get = EquivRules.get |
187 val equiv_rules_add = EquivRules.add |
188 val equiv_rules_add = EquivRules.add |
188 |
189 |
189 (* respectfulness theorems *) |
190 (* respectfulness theorems *) |
190 structure RspRules = Named_Thms |
191 structure RspRules = Named_Thms |
191 (val name = "quotient_rsp" |
192 (val name = "quot_respect" |
192 val description = "Respectfulness theorems.") |
193 val description = "Respectfulness theorems.") |
193 |
194 |
194 val rsp_rules_get = RspRules.get |
195 val rsp_rules_get = RspRules.get |
|
196 |
|
197 (* preservation theorems *) |
|
198 structure PrsRules = Named_Thms |
|
199 (val name = "quot_preserve" |
|
200 val description = "Respectfulness theorems.") |
|
201 |
|
202 val prs_rules_get = PrsRules.get |
195 |
203 |
196 (* respectfulness theorems *) |
204 (* respectfulness theorems *) |
197 structure IdSimps = Named_Thms |
205 structure IdSimps = Named_Thms |
198 (val name = "id_simps" |
206 (val name = "id_simps" |
199 val description = "Identity simp rules for maps.") |
207 val description = "Identity simp rules for maps.") |
200 |
208 |
201 val id_simps_get = IdSimps.get |
209 val id_simps_get = IdSimps.get |
202 |
210 |
203 (* quotient theorems *) |
211 (* quotient theorems *) |
204 structure QuotientRules = Named_Thms |
212 structure QuotientRules = Named_Thms |
205 (val name = "quotient_thm" |
213 (val name = "quot_thm" |
206 val description = "Quotient theorems.") |
214 val description = "Quotient theorems.") |
207 |
215 |
208 val quotient_rules_get = QuotientRules.get |
216 val quotient_rules_get = QuotientRules.get |
209 val quotient_rules_add = QuotientRules.add |
217 val quotient_rules_add = QuotientRules.add |
210 |
218 |