43 |
43 |
44 val maps_lookup = Symtab.lookup o MapsData.get |
44 val maps_lookup = Symtab.lookup o MapsData.get |
45 |
45 |
46 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo)) |
46 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo)) |
47 fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo) |
47 fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo) |
|
48 (* FIXME: this should be done using a generic context *) |
48 |
49 |
49 fun maps_attribute_aux s minfo = Thm.declaration_attribute |
50 fun maps_attribute_aux s minfo = Thm.declaration_attribute |
50 (fn thm => Context.mapping (maps_update_thy s minfo) (maps_update s minfo)) |
51 (fn thm => Context.mapping (maps_update_thy s minfo) (maps_update s minfo)) |
51 |
52 |
52 (* attribute to be used in declare statements *) |
53 (* attribute to be used in declare statements *) |
93 |
94 |
94 fun print_quotinfo ctxt = |
95 fun print_quotinfo ctxt = |
95 let |
96 let |
96 fun prt_quot {qtyp, rtyp, rel, equiv_thm} = |
97 fun prt_quot {qtyp, rtyp, rel, equiv_thm} = |
97 Pretty.block (Library.separate (Pretty.brk 2) |
98 Pretty.block (Library.separate (Pretty.brk 2) |
98 [Pretty.str ("quotient type:"), |
99 [Pretty.str "quotient type:", |
99 Syntax.pretty_typ ctxt qtyp, |
100 Syntax.pretty_typ ctxt qtyp, |
100 Pretty.str ("raw type:"), |
101 Pretty.str "raw type:", |
101 Syntax.pretty_typ ctxt rtyp, |
102 Syntax.pretty_typ ctxt rtyp, |
102 Pretty.str ("relation:"), |
103 Pretty.str "relation:", |
103 Syntax.pretty_term ctxt rel, |
104 Syntax.pretty_term ctxt rel, |
104 Pretty.str ("equiv. thm:"), |
105 Pretty.str "equiv. thm:", |
105 Syntax.pretty_term ctxt (prop_of equiv_thm)]) |
106 Syntax.pretty_term ctxt (prop_of equiv_thm)]) |
106 in |
107 in |
107 QuotData.get (ProofContext.theory_of ctxt) |
108 QuotData.get (ProofContext.theory_of ctxt) |
108 |> Symtab.dest |
109 |> Symtab.dest |
109 |> map (prt_quot o snd) |
110 |> map (prt_quot o snd) |
146 rconst = Morphism.term phi rconst} |
147 rconst = Morphism.term phi rconst} |
147 |
148 |
148 val qconsts_lookup = Symtab.lookup o QConstsData.get |
149 val qconsts_lookup = Symtab.lookup o QConstsData.get |
149 |
150 |
150 fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo)) |
151 fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo)) |
151 fun qconsts_update_gen k qcinfo = |
152 fun qconsts_update_gen k qcinfo = Context.mapping (qconsts_update_thy k qcinfo) I |
152 Context.mapping (qconsts_update_thy k qcinfo) I |
|
153 |
153 |
154 fun print_qconstinfo ctxt = |
154 fun print_qconstinfo ctxt = |
155 let |
155 let |
156 fun prt_qconst {qconst, rconst} = |
156 fun prt_qconst {qconst, rconst} = |
157 Pretty.block (separate (Pretty.brk 1) |
157 Pretty.block (separate (Pretty.brk 1) |