9 val print_quotinfo: Proof.context -> unit |
9 val print_quotinfo: Proof.context -> unit |
10 val quotdata_lookup_thy: theory -> string -> quotient_info option |
10 val quotdata_lookup_thy: theory -> string -> quotient_info option |
11 val quotdata_lookup: Proof.context -> string -> quotient_info option |
11 val quotdata_lookup: Proof.context -> string -> quotient_info option |
12 val quotdata_update_thy: string -> (typ * typ * term * thm) -> theory -> theory |
12 val quotdata_update_thy: string -> (typ * typ * term * thm) -> theory -> theory |
13 val quotdata_update: string -> (typ * typ * term * thm) -> Proof.context -> Proof.context |
13 val quotdata_update: string -> (typ * typ * term * thm) -> Proof.context -> Proof.context |
|
14 val quotdata_dest: theory -> quotient_info list |
14 |
15 |
15 type qconsts_info = {qconst: term, rconst: term} |
16 type qconsts_info = {qconst: term, rconst: term} |
16 val qconsts_transfer: morphism -> qconsts_info -> qconsts_info |
17 val qconsts_transfer: morphism -> qconsts_info -> qconsts_info |
17 val qconsts_lookup: theory -> string -> qconsts_info option |
18 val qconsts_lookup: theory -> string -> qconsts_info option |
18 val qconsts_update_thy: string -> qconsts_info -> theory -> theory |
19 val qconsts_update_thy: string -> qconsts_info -> theory -> theory |
86 QuotData.map (Symtab.update (qty_name, {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm})) |
87 QuotData.map (Symtab.update (qty_name, {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm})) |
87 |
88 |
88 fun quotdata_update qty_name (qty, rty, rel, equiv_thm) = |
89 fun quotdata_update qty_name (qty, rty, rel, equiv_thm) = |
89 ProofContext.theory (quotdata_update_thy qty_name (qty, rty, rel, equiv_thm)) |
90 ProofContext.theory (quotdata_update_thy qty_name (qty, rty, rel, equiv_thm)) |
90 |
91 |
|
92 fun quotdata_dest thy = |
|
93 map snd (Symtab.dest (QuotData.get thy)) |
|
94 |
91 fun print_quotinfo ctxt = |
95 fun print_quotinfo ctxt = |
92 let |
96 let |
93 fun prt_quot {qtyp, rtyp, rel, equiv_thm} = |
97 fun prt_quot {qtyp, rtyp, rel, equiv_thm} = |
94 Pretty.block (Library.separate (Pretty.brk 2) |
98 Pretty.block (Library.separate (Pretty.brk 2) |
95 [Pretty.str "quotient type:", |
99 [Pretty.str "quotient type:", |