7 val maps_update_thy: string -> maps_info -> theory -> theory |
7 val maps_update_thy: string -> maps_info -> theory -> theory |
8 val maps_update: string -> maps_info -> Proof.context -> Proof.context |
8 val maps_update: string -> maps_info -> Proof.context -> Proof.context |
9 val print_mapsinfo: Proof.context -> unit |
9 val print_mapsinfo: Proof.context -> unit |
10 |
10 |
11 type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm} |
11 type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm} |
12 val quotdata_transfer: morphism -> quotdata_info -> quotdata_info |
12 val transform_quotdata: morphism -> quotdata_info -> quotdata_info |
13 val quotdata_lookup: theory -> string -> quotdata_info (* raises NotFound *) |
13 val quotdata_lookup: theory -> string -> quotdata_info (* raises NotFound *) |
14 val quotdata_update_thy: string -> quotdata_info -> theory -> theory |
14 val quotdata_update_thy: string -> quotdata_info -> theory -> theory |
15 val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic |
15 val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic |
16 val print_quotinfo: Proof.context -> unit |
16 val print_quotinfo: Proof.context -> unit |
17 |
17 |
18 type qconsts_info = {qconst: term, rconst: term, def: thm} |
18 type qconsts_info = {qconst: term, rconst: term, def: thm} |
19 val qconsts_transfer: morphism -> qconsts_info -> qconsts_info |
19 val transform_qconsts: morphism -> qconsts_info -> qconsts_info |
20 val qconsts_lookup: theory -> term -> qconsts_info (* raises NotFound *) |
20 val qconsts_lookup: theory -> term -> qconsts_info (* raises NotFound *) |
21 val qconsts_update_thy: string -> qconsts_info -> theory -> theory |
21 val qconsts_update_thy: string -> qconsts_info -> theory -> theory |
22 val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic |
22 val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic |
23 val qconsts_dest: theory -> qconsts_info list |
23 val qconsts_dest: theory -> qconsts_info list |
24 val print_qconstinfo: Proof.context -> unit |
24 val print_qconstinfo: Proof.context -> unit |
136 (type T = quotdata_info Symtab.table |
136 (type T = quotdata_info Symtab.table |
137 val empty = Symtab.empty |
137 val empty = Symtab.empty |
138 val extend = I |
138 val extend = I |
139 val merge = Symtab.merge (K true)) |
139 val merge = Symtab.merge (K true)) |
140 |
140 |
141 fun quotdata_transfer phi {qtyp, rtyp, equiv_rel, equiv_thm} = |
141 fun transform_quotdata phi {qtyp, rtyp, equiv_rel, equiv_thm} = |
142 {qtyp = Morphism.typ phi qtyp, |
142 {qtyp = Morphism.typ phi qtyp, |
143 rtyp = Morphism.typ phi rtyp, |
143 rtyp = Morphism.typ phi rtyp, |
144 equiv_rel = Morphism.term phi equiv_rel, |
144 equiv_rel = Morphism.term phi equiv_rel, |
145 equiv_thm = Morphism.thm phi equiv_thm} |
145 equiv_thm = Morphism.thm phi equiv_thm} |
146 |
146 |
183 (type T = qconsts_info Symtab.table |
183 (type T = qconsts_info Symtab.table |
184 val empty = Symtab.empty |
184 val empty = Symtab.empty |
185 val extend = I |
185 val extend = I |
186 val merge = Symtab.merge (K true)) |
186 val merge = Symtab.merge (K true)) |
187 |
187 |
188 fun qconsts_transfer phi {qconst, rconst, def} = |
188 fun transform_qconsts phi {qconst, rconst, def} = |
189 {qconst = Morphism.term phi qconst, |
189 {qconst = Morphism.term phi qconst, |
190 rconst = Morphism.term phi rconst, |
190 rconst = Morphism.term phi rconst, |
191 def = Morphism.thm phi def} |
191 def = Morphism.thm phi def} |
192 |
192 |
193 fun qconsts_update_thy str qcinfo = QConstsData.map (Symtab.update (str, qcinfo)) |
193 fun qconsts_update_thy str qcinfo = QConstsData.map (Symtab.update (str, qcinfo)) |