equal
deleted
inserted
replaced
9 val maps_update: string -> maps_info -> Proof.context -> Proof.context |
9 val maps_update: string -> maps_info -> Proof.context -> Proof.context |
10 val print_mapsinfo: Proof.context -> unit |
10 val print_mapsinfo: Proof.context -> unit |
11 |
11 |
12 type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm} |
12 type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm} |
13 val transform_quotdata: morphism -> quotdata_info -> quotdata_info |
13 val transform_quotdata: morphism -> quotdata_info -> quotdata_info |
|
14 val quotdata_lookup_raw: theory -> string -> quotdata_info option |
14 val quotdata_lookup: theory -> string -> quotdata_info (* raises NotFound *) |
15 val quotdata_lookup: theory -> string -> quotdata_info (* raises NotFound *) |
15 val quotdata_update_thy: string -> quotdata_info -> theory -> theory |
16 val quotdata_update_thy: string -> quotdata_info -> theory -> theory |
16 val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic |
17 val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic |
17 val print_quotinfo: Proof.context -> unit |
18 val print_quotinfo: Proof.context -> unit |
18 |
19 |
145 {qtyp = Morphism.typ phi qtyp, |
146 {qtyp = Morphism.typ phi qtyp, |
146 rtyp = Morphism.typ phi rtyp, |
147 rtyp = Morphism.typ phi rtyp, |
147 equiv_rel = Morphism.term phi equiv_rel, |
148 equiv_rel = Morphism.term phi equiv_rel, |
148 equiv_thm = Morphism.thm phi equiv_thm} |
149 equiv_thm = Morphism.thm phi equiv_thm} |
149 |
150 |
150 fun quotdata_lookup thy str = |
151 fun quotdata_lookup_raw thy str = Symtab.lookup (QuotData.get thy) str |
|
152 |
|
153 fun quotdata_lookup thy str = |
151 case Symtab.lookup (QuotData.get thy) str of |
154 case Symtab.lookup (QuotData.get thy) str of |
152 SOME qinfo => qinfo |
155 SOME qinfo => qinfo |
153 | NONE => raise NotFound |
156 | NONE => raise NotFound |
154 |
157 |
155 fun quotdata_update_thy str qinfo = QuotData.map (Symtab.update (str, qinfo)) |
158 fun quotdata_update_thy str qinfo = QuotData.map (Symtab.update (str, qinfo)) |