equal
deleted
inserted
replaced
19 val qconsts_update_thy: string -> qconsts_info -> theory -> theory |
19 val qconsts_update_thy: string -> qconsts_info -> theory -> theory |
20 val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic |
20 val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic |
21 val print_qconstinfo: Proof.context -> unit |
21 val print_qconstinfo: Proof.context -> unit |
22 |
22 |
23 val rsp_rules_get: Proof.context -> thm list |
23 val rsp_rules_get: Proof.context -> thm list |
|
24 val quotient_rules_get: Proof.context -> thm list |
|
25 val quotient_rules_add: attribute |
24 end; |
26 end; |
25 |
27 |
26 structure Quotient_Info: QUOTIENT_INFO = |
28 structure Quotient_Info: QUOTIENT_INFO = |
27 struct |
29 struct |
28 |
30 |
159 (val name = "quot_rsp" |
161 (val name = "quot_rsp" |
160 val description = "Respectfulness theorems.") |
162 val description = "Respectfulness theorems.") |
161 |
163 |
162 val rsp_rules_get = RspRules.get |
164 val rsp_rules_get = RspRules.get |
163 |
165 |
164 val _ = Context.>> (Context.map_theory RspRules.setup) |
166 (* quotient lemmas *) |
|
167 structure QuotientRules = Named_Thms |
|
168 (val name = "quotient" |
|
169 val description = "Quotient theorems.") |
|
170 |
|
171 val quotient_rules_get = QuotientRules.get |
|
172 val quotient_rules_add = Thm.declaration_attribute QuotientRules.add_thm |
|
173 |
|
174 (* setup of the theorem lists *) |
|
175 val _ = Context.>> (Context.map_theory |
|
176 (RspRules.setup #> |
|
177 QuotientRules.setup)) |
165 |
178 |
166 end; (* structure *) |
179 end; (* structure *) |
167 |
180 |
168 open Quotient_Info |
181 open Quotient_Info |