4 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} |
4 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} |
5 val mk_quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state |
5 val mk_quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state |
6 val mk_quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state |
6 val mk_quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state |
7 val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory |
7 val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory |
8 val note: binding * thm -> local_theory -> thm * local_theory |
8 val note: binding * thm -> local_theory -> thm * local_theory |
9 val maps_lookup_thy: theory -> string -> maps_info option |
9 val maps_lookup: theory -> string -> maps_info option |
10 val maps_update_thy: string -> maps_info -> theory -> theory |
10 val maps_update_thy: string -> maps_info -> theory -> theory |
11 val maps_update: string -> maps_info -> Proof.context -> Proof.context |
11 val maps_update: string -> maps_info -> Proof.context -> Proof.context |
12 val print_quotdata: Proof.context -> unit |
12 val print_quotdata: Proof.context -> unit |
13 val quotdata_lookup_thy: theory -> quotient_info list |
13 val quotdata_lookup_thy: theory -> quotient_info list |
14 val quotdata_lookup: Proof.context -> quotient_info list |
14 val quotdata_lookup: Proof.context -> quotient_info list |
30 val empty = Symtab.empty |
30 val empty = Symtab.empty |
31 val copy = I |
31 val copy = I |
32 val extend = I |
32 val extend = I |
33 fun merge _ = Symtab.merge (K true)) |
33 fun merge _ = Symtab.merge (K true)) |
34 |
34 |
35 val maps_lookup_thy = Symtab.lookup o MapsData.get |
35 val maps_lookup = Symtab.lookup o MapsData.get |
36 |
36 |
37 |
37 |
38 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo)) |
38 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo)) |
39 fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo) |
39 fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo) |
40 |
40 |