equal
deleted
inserted
replaced
36 structure Quotient_Info: QUOTIENT_INFO = |
36 structure Quotient_Info: QUOTIENT_INFO = |
37 struct |
37 struct |
38 |
38 |
39 exception NotFound |
39 exception NotFound |
40 |
40 |
|
41 (*******************) |
41 (* data containers *) |
42 (* data containers *) |
42 (*******************) |
43 (*******************) |
43 |
44 |
44 (* info about map- and rel-functions for a type *) |
45 (* info about map- and rel-functions for a type *) |
45 type maps_info = {mapfun: string, relfun: string} |
46 type maps_info = {mapfun: string, relfun: string} |
101 |> map (prt_map) |
102 |> map (prt_map) |
102 |> Pretty.big_list "maps:" |
103 |> Pretty.big_list "maps:" |
103 |> Pretty.writeln |
104 |> Pretty.writeln |
104 end |
105 end |
105 |
106 |
|
107 val _ = |
|
108 OuterSyntax.improper_command "print_maps" "prints out all map functions" |
|
109 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_mapsinfo o Toplevel.context_of))) |
106 |
110 |
107 |
111 |
108 (* info about quotient types *) |
112 (* info about quotient types *) |
109 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} |
113 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} |
110 |
114 |
147 |> Pretty.big_list "quotients:" |
151 |> Pretty.big_list "quotients:" |
148 |> Pretty.writeln |
152 |> Pretty.writeln |
149 end |
153 end |
150 |
154 |
151 val _ = |
155 val _ = |
152 OuterSyntax.improper_command "print_quotients" "print out all quotients" |
156 OuterSyntax.improper_command "print_quotients" "prints out all quotients" |
153 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of))) |
157 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of))) |
154 |
158 |
155 |
159 |
156 (* info about quotient constants *) |
160 (* info about quotient constants *) |
157 type qconsts_info = {qconst: term, rconst: term, def: thm} |
161 type qconsts_info = {qconst: term, rconst: term, def: thm} |
207 |> Pretty.big_list "quotient constants:" |
211 |> Pretty.big_list "quotient constants:" |
208 |> Pretty.writeln |
212 |> Pretty.writeln |
209 end |
213 end |
210 |
214 |
211 val _ = |
215 val _ = |
212 OuterSyntax.improper_command "print_quotconsts" "print out all quotient constants" |
216 OuterSyntax.improper_command "print_quotconsts" "prints out all quotient constants" |
213 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of))) |
217 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of))) |
214 |
218 |
215 (* FIXME/TODO: check the various lemmas conform *) |
219 (* FIXME/TODO: check the various lemmas conform *) |
216 (* with the required shape *) |
220 (* with the required shape *) |
217 |
221 |
231 val rsp_rules_get = RspRules.get |
235 val rsp_rules_get = RspRules.get |
232 |
236 |
233 (* preservation theorems *) |
237 (* preservation theorems *) |
234 structure PrsRules = Named_Thms |
238 structure PrsRules = Named_Thms |
235 (val name = "quot_preserve" |
239 (val name = "quot_preserve" |
236 val description = "Respectfulness theorems.") |
240 val description = "Preservation theorems.") |
237 |
241 |
238 val prs_rules_get = PrsRules.get |
242 val prs_rules_get = PrsRules.get |
239 |
243 |
240 (* id simplification theorems *) |
244 (* id simplification theorems *) |
241 structure IdSimps = Named_Thms |
245 structure IdSimps = Named_Thms |