21 val qconsts_update_thy: string -> qconsts_info -> theory -> theory |
21 val qconsts_update_thy: string -> qconsts_info -> theory -> theory |
22 val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic |
22 val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic |
23 val qconsts_dest: theory -> qconsts_info list |
23 val qconsts_dest: theory -> qconsts_info list |
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 |
|
27 val equiv_rules_add: attribute |
26 val rsp_rules_get: Proof.context -> thm list |
28 val rsp_rules_get: Proof.context -> thm list |
27 val quotient_rules_get: Proof.context -> thm list |
29 val quotient_rules_get: Proof.context -> thm list |
28 val quotient_rules_add: attribute |
30 val quotient_rules_add: attribute |
29 end; |
31 end; |
30 |
32 |
166 |
168 |
167 val _ = |
169 val _ = |
168 OuterSyntax.improper_command "print_quotconsts" "print out all quotient constants" |
170 OuterSyntax.improper_command "print_quotconsts" "print out all quotient constants" |
169 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of))) |
171 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of))) |
170 |
172 |
171 (* respectfulness lemmas *) |
173 (* equivalence relation theorems *) |
|
174 structure EquivRules = Named_Thms |
|
175 (val name = "quotient_equiv" |
|
176 val description = "Equivalence relation theorems.") |
|
177 |
|
178 val equiv_rules_get = EquivRules.get |
|
179 val equiv_rules_add = EquivRules.add |
|
180 |
|
181 (* respectfulness theorems *) |
172 structure RspRules = Named_Thms |
182 structure RspRules = Named_Thms |
173 (val name = "quotient_rsp" |
183 (val name = "quotient_rsp" |
174 val description = "Respectfulness theorems.") |
184 val description = "Respectfulness theorems.") |
175 |
185 |
176 val rsp_rules_get = RspRules.get |
186 val rsp_rules_get = RspRules.get |
177 |
187 |
178 (* quotient lemmas *) |
188 (* quotient theorems *) |
179 structure QuotientRules = Named_Thms |
189 structure QuotientRules = Named_Thms |
180 (val name = "quotient_thm" |
190 (val name = "quotient_thm" |
181 val description = "Quotient theorems.") |
191 val description = "Quotient theorems.") |
182 |
192 |
183 val quotient_rules_get = QuotientRules.get |
193 val quotient_rules_get = QuotientRules.get |
184 val quotient_rules_add = Thm.declaration_attribute QuotientRules.add_thm |
194 val quotient_rules_add = QuotientRules.add |
185 |
195 |
186 (* setup of the theorem lists *) |
196 (* setup of the theorem lists *) |
187 val _ = Context.>> (Context.map_theory |
197 val _ = Context.>> (Context.map_theory |
188 (RspRules.setup #> |
198 (EquivRules.setup #> |
|
199 RspRules.setup #> |
189 QuotientRules.setup)) |
200 QuotientRules.setup)) |
190 |
201 |
191 end; (* structure *) |
202 end; (* structure *) |
192 |
203 |
193 open Quotient_Info |
204 open Quotient_Info |