equal
deleted
inserted
replaced
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 id_simps_get: Proof.context -> thm list |
29 val quotient_rules_get: Proof.context -> thm list |
30 val quotient_rules_get: Proof.context -> thm list |
30 val quotient_rules_add: attribute |
31 val quotient_rules_add: attribute |
31 end; |
32 end; |
32 |
33 |
33 structure Quotient_Info: QUOTIENT_INFO = |
34 structure Quotient_Info: QUOTIENT_INFO = |
172 |
173 |
173 val _ = |
174 val _ = |
174 OuterSyntax.improper_command "print_quotconsts" "print out all quotient constants" |
175 OuterSyntax.improper_command "print_quotconsts" "print out all quotient constants" |
175 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of))) |
176 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of))) |
176 |
177 |
|
178 (* FIXME/TODO: check the various lemmas conform *) |
|
179 (* with the required shape *) |
|
180 |
177 (* equivalence relation theorems *) |
181 (* equivalence relation theorems *) |
178 structure EquivRules = Named_Thms |
182 structure EquivRules = Named_Thms |
179 (val name = "quotient_equiv" |
183 (val name = "quotient_equiv" |
180 val description = "Equivalence relation theorems.") |
184 val description = "Equivalence relation theorems.") |
181 |
185 |
187 (val name = "quotient_rsp" |
191 (val name = "quotient_rsp" |
188 val description = "Respectfulness theorems.") |
192 val description = "Respectfulness theorems.") |
189 |
193 |
190 val rsp_rules_get = RspRules.get |
194 val rsp_rules_get = RspRules.get |
191 |
195 |
|
196 (* respectfulness theorems *) |
|
197 structure IdSimps = Named_Thms |
|
198 (val name = "id_simps" |
|
199 val description = "Identity simp rules for maps.") |
|
200 |
|
201 val id_simps_get = IdSimps.get |
|
202 |
192 (* quotient theorems *) |
203 (* quotient theorems *) |
193 structure QuotientRules = Named_Thms |
204 structure QuotientRules = Named_Thms |
194 (val name = "quotient_thm" |
205 (val name = "quotient_thm" |
195 val description = "Quotient theorems.") |
206 val description = "Quotient theorems.") |
196 |
207 |
199 |
210 |
200 (* setup of the theorem lists *) |
211 (* setup of the theorem lists *) |
201 val _ = Context.>> (Context.map_theory |
212 val _ = Context.>> (Context.map_theory |
202 (EquivRules.setup #> |
213 (EquivRules.setup #> |
203 RspRules.setup #> |
214 RspRules.setup #> |
|
215 IdSimps.setup #> |
204 QuotientRules.setup)) |
216 QuotientRules.setup)) |
205 |
217 |
206 end; (* structure *) |
218 end; (* structure *) |
207 |
219 |
208 open Quotient_Info |
220 open Quotient_Info |