equal
deleted
inserted
replaced
162 OuterSyntax.improper_command "print_quotconsts" "print out all quotient constants" |
162 OuterSyntax.improper_command "print_quotconsts" "print out all quotient constants" |
163 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of))) |
163 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of))) |
164 |
164 |
165 (* respectfulness lemmas *) |
165 (* respectfulness lemmas *) |
166 structure RspRules = Named_Thms |
166 structure RspRules = Named_Thms |
167 (val name = "quot_rsp" |
167 (val name = "quotient_rsp" |
168 val description = "Respectfulness theorems.") |
168 val description = "Respectfulness theorems.") |
169 |
169 |
170 val rsp_rules_get = RspRules.get |
170 val rsp_rules_get = RspRules.get |
171 |
171 |
172 (* quotient lemmas *) |
172 (* quotient lemmas *) |
173 structure QuotientRules = Named_Thms |
173 structure QuotientRules = Named_Thms |
174 (val name = "quotient" |
174 (val name = "quotient_thm" |
175 val description = "Quotient theorems.") |
175 val description = "Quotient theorems.") |
176 |
176 |
177 val quotient_rules_get = QuotientRules.get |
177 val quotient_rules_get = QuotientRules.get |
178 val quotient_rules_add = Thm.declaration_attribute QuotientRules.add_thm |
178 val quotient_rules_add = Thm.declaration_attribute QuotientRules.add_thm |
179 |
179 |