equal
deleted
inserted
replaced
39 exception NotFound |
39 exception NotFound |
40 |
40 |
41 (* data containers *) |
41 (* data containers *) |
42 (*******************) |
42 (*******************) |
43 |
43 |
44 (* info about map- and rel-functions *) |
44 (* info about map- and rel-functions for a type *) |
45 type maps_info = {mapfun: string, relfun: string} |
45 type maps_info = {mapfun: string, relfun: string} |
46 |
46 |
47 structure MapsData = Theory_Data |
47 structure MapsData = Theory_Data |
48 (type T = maps_info Symtab.table |
48 (type T = maps_info Symtab.table |
49 val empty = Symtab.empty |
49 val empty = Symtab.empty |
186 case (find_first matches smt) of |
186 case (find_first matches smt) of |
187 SOME (_, x) => x |
187 SOME (_, x) => x |
188 | _ => raise NotFound |
188 | _ => raise NotFound |
189 end |
189 end |
190 |
190 |
191 (* We don't print the definition *) |
191 (* We omit printing the definition *) |
192 fun print_qconstinfo ctxt = |
192 fun print_qconstinfo ctxt = |
193 let |
193 let |
194 fun prt_qconst {qconst, rconst, def} = |
194 fun prt_qconst {qconst, rconst, def} = |
195 Pretty.block (separate (Pretty.brk 1) |
195 Pretty.block (separate (Pretty.brk 1) |
196 [Syntax.pretty_term ctxt qconst, |
196 [Syntax.pretty_term ctxt qconst, |
231 (val name = "quot_preserve" |
231 (val name = "quot_preserve" |
232 val description = "Respectfulness theorems.") |
232 val description = "Respectfulness theorems.") |
233 |
233 |
234 val prs_rules_get = PrsRules.get |
234 val prs_rules_get = PrsRules.get |
235 |
235 |
236 (* respectfulness theorems *) |
236 (* id simplification theorems *) |
237 structure IdSimps = Named_Thms |
237 structure IdSimps = Named_Thms |
238 (val name = "id_simps" |
238 (val name = "id_simps" |
239 val description = "Identity simp rules for maps.") |
239 val description = "Identity simp rules for maps.") |
240 |
240 |
241 val id_simps_get = IdSimps.get |
241 val id_simps_get = IdSimps.get |