equal
deleted
inserted
replaced
16 val qconsts_transfer: morphism -> qconsts_info -> qconsts_info |
16 val qconsts_transfer: morphism -> qconsts_info -> qconsts_info |
17 val qconsts_lookup: theory -> string -> qconsts_info option |
17 val qconsts_lookup: theory -> string -> qconsts_info option |
18 val qconsts_update_thy: string -> qconsts_info -> theory -> theory |
18 val qconsts_update_thy: string -> qconsts_info -> theory -> theory |
19 val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic |
19 val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic |
20 val print_qconstinfo: Proof.context -> unit |
20 val print_qconstinfo: Proof.context -> unit |
|
21 |
|
22 val rsp_rules_get: Proof.context -> thm list |
21 end; |
23 end; |
22 |
24 |
23 structure Quotient_Info: QUOTIENT_INFO = |
25 structure Quotient_Info: QUOTIENT_INFO = |
24 struct |
26 struct |
25 |
27 |
109 val _ = |
111 val _ = |
110 OuterSyntax.improper_command "print_quotients" "print out all quotients" |
112 OuterSyntax.improper_command "print_quotients" "print out all quotients" |
111 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of))) |
113 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of))) |
112 |
114 |
113 |
115 |
114 (* information about quotient constants *) |
116 (* info about quotient constants *) |
115 type qconsts_info = {qconst: term, rconst: term} |
117 type qconsts_info = {qconst: term, rconst: term} |
116 |
118 |
117 structure QConstsData = Theory_Data |
119 structure QConstsData = Theory_Data |
118 (type T = qconsts_info Symtab.table |
120 (type T = qconsts_info Symtab.table |
119 val empty = Symtab.empty |
121 val empty = Symtab.empty |
146 |
148 |
147 val _ = |
149 val _ = |
148 OuterSyntax.improper_command "print_quotconsts" "print out all quotient constants" |
150 OuterSyntax.improper_command "print_quotconsts" "print out all quotient constants" |
149 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of))) |
151 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of))) |
150 |
152 |
|
153 (* respectfulness lemmas *) |
|
154 structure RspRules = Named_Thms |
|
155 (val name = "quot_rsp" |
|
156 val description = "Respectfulness theorems.") |
|
157 |
|
158 val rsp_rules_get = RspRules.get |
|
159 |
|
160 val _ = Context.>> (Context.map_theory RspRules.setup) |
|
161 |
151 end; (* structure *) |
162 end; (* structure *) |
152 |
163 |
153 open Quotient_Info |
164 open Quotient_Info |