equal
deleted
inserted
replaced
8 val note: binding * thm -> local_theory -> thm * local_theory |
8 val note: binding * thm -> local_theory -> thm * local_theory |
9 val maps_lookup: 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: 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_update_thy: (typ * typ * term * thm) -> theory -> theory |
15 val quotdata_update_thy: (typ * typ * term * thm) -> theory -> theory |
15 val quotdata_update: (typ * typ * term * thm) -> Proof.context -> Proof.context |
16 val quotdata_update: (typ * typ * term * thm) -> Proof.context -> Proof.context |
16 end; |
17 end; |
17 |
18 |
18 structure Quotient: QUOTIENT = |
19 structure Quotient: QUOTIENT = |
68 val empty = [] |
69 val empty = [] |
69 val copy = I |
70 val copy = I |
70 val extend = I |
71 val extend = I |
71 fun merge _ = (op @)) (* FIXME: is this the correct merging function for the list? *) |
72 fun merge _ = (op @)) (* FIXME: is this the correct merging function for the list? *) |
72 |
73 |
73 val quotdata_lookup = QuotData.get |
74 val quotdata_lookup_thy = QuotData.get |
|
75 val quotdata_lookup = QuotData.get o ProofContext.theory_of |
74 |
76 |
75 fun quotdata_update_thy (qty, rty, rel, equiv_thm) thy = |
77 fun quotdata_update_thy (qty, rty, rel, equiv_thm) thy = |
76 QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm}::ls) thy |
78 QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm}::ls) thy |
77 |
79 |
78 fun quotdata_update (qty, rty, rel, equiv_thm) ctxt = |
80 fun quotdata_update (qty, rty, rel, equiv_thm) ctxt = |