equal
deleted
inserted
replaced
21 val transform_quotdata: morphism -> quotdata_info -> quotdata_info |
21 val transform_quotdata: morphism -> quotdata_info -> quotdata_info |
22 val quotdata_lookup_raw: theory -> string -> quotdata_info option |
22 val quotdata_lookup_raw: theory -> string -> quotdata_info option |
23 val quotdata_lookup: theory -> string -> quotdata_info (* raises NotFound *) |
23 val quotdata_lookup: theory -> string -> quotdata_info (* raises NotFound *) |
24 val quotdata_update_thy: string -> quotdata_info -> theory -> theory |
24 val quotdata_update_thy: string -> quotdata_info -> theory -> theory |
25 val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic |
25 val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic |
|
26 val quotdata_dest: Proof.context -> quotdata_info list |
26 val print_quotinfo: Proof.context -> unit |
27 val print_quotinfo: Proof.context -> unit |
27 |
28 |
28 type qconsts_info = {qconst: term, rconst: term, def: thm} |
29 type qconsts_info = {qconst: term, rconst: term, def: thm} |
29 val transform_qconsts: morphism -> qconsts_info -> qconsts_info |
30 val transform_qconsts: morphism -> qconsts_info -> qconsts_info |
30 val qconsts_lookup: theory -> term -> qconsts_info (* raises NotFound *) |
31 val qconsts_lookup: theory -> term -> qconsts_info (* raises NotFound *) |
163 SOME qinfo => qinfo |
164 SOME qinfo => qinfo |
164 | NONE => raise NotFound |
165 | NONE => raise NotFound |
165 |
166 |
166 fun quotdata_update_thy str qinfo = QuotData.map (Symtab.update (str, qinfo)) |
167 fun quotdata_update_thy str qinfo = QuotData.map (Symtab.update (str, qinfo)) |
167 fun quotdata_update_gen str qinfo = Context.mapping (quotdata_update_thy str qinfo) I |
168 fun quotdata_update_gen str qinfo = Context.mapping (quotdata_update_thy str qinfo) I |
|
169 |
|
170 fun quotdata_dest lthy = |
|
171 map snd (Symtab.dest (QuotData.get (ProofContext.theory_of lthy))) |
168 |
172 |
169 fun print_quotinfo ctxt = |
173 fun print_quotinfo ctxt = |
170 let |
174 let |
171 fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} = |
175 fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} = |
172 Pretty.block (Library.separate (Pretty.brk 2) |
176 Pretty.block (Library.separate (Pretty.brk 2) |