equal
deleted
inserted
replaced
18 |
18 |
19 type qconsts_info = {qconst: term, rconst: term} |
19 type qconsts_info = {qconst: term, rconst: term} |
20 val qconsts_transfer: morphism -> qconsts_info -> qconsts_info |
20 val qconsts_transfer: morphism -> qconsts_info -> qconsts_info |
21 val qconsts_lookup: theory -> string -> qconsts_info option |
21 val qconsts_lookup: theory -> string -> qconsts_info option |
22 val qconsts_update_thy: string -> qconsts_info -> theory -> theory |
22 val qconsts_update_thy: string -> qconsts_info -> theory -> theory |
23 val qconsts_update_generic: string -> qconsts_info -> Context.generic -> Context.generic |
23 val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic |
24 val print_qconstinfo: Proof.context -> unit |
24 val print_qconstinfo: Proof.context -> unit |
25 end; |
25 end; |
26 |
26 |
27 structure Quotient_Info: QUOTIENT_INFO = |
27 structure Quotient_Info: QUOTIENT_INFO = |
28 struct |
28 struct |
145 rconst = Morphism.term phi rconst} |
145 rconst = Morphism.term phi rconst} |
146 |
146 |
147 val qconsts_lookup = Symtab.lookup o QConstsData.get |
147 val qconsts_lookup = Symtab.lookup o QConstsData.get |
148 |
148 |
149 fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo)) |
149 fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo)) |
150 fun qconsts_update_generic k qcinfo = |
150 fun qconsts_update_gen k qcinfo = |
151 Context.mapping (qconsts_update_thy k qcinfo) I |
151 Context.mapping (qconsts_update_thy k qcinfo) I |
152 |
152 |
153 fun print_qconstinfo ctxt = |
153 fun print_qconstinfo ctxt = |
154 let |
154 let |
155 fun prt_qconst {qconst, rconst} = |
155 fun prt_qconst {qconst, rconst} = |