equal
deleted
inserted
replaced
25 (*******************) |
25 (*******************) |
26 |
26 |
27 (* info about map- and rel-functions *) |
27 (* info about map- and rel-functions *) |
28 type maps_info = {mapfun: string, relfun: string} |
28 type maps_info = {mapfun: string, relfun: string} |
29 |
29 |
30 structure MapsData = TheoryDataFun |
30 structure MapsData = Theory_Data |
31 (type T = maps_info Symtab.table |
31 (type T = maps_info Symtab.table |
32 val empty = Symtab.empty |
32 val empty = Symtab.empty |
33 val copy = I |
|
34 val extend = I |
33 val extend = I |
35 fun merge _ = Symtab.merge (K true)) |
34 val merge = Symtab.merge (K true)) |
36 |
35 |
37 val maps_lookup = Symtab.lookup o MapsData.get |
36 val maps_lookup = Symtab.lookup o MapsData.get |
38 |
37 |
39 |
38 |
40 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo)) |
39 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo)) |
66 |
65 |
67 |
66 |
68 (* info about the quotient types *) |
67 (* info about the quotient types *) |
69 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} |
68 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} |
70 |
69 |
71 structure QuotData = TheoryDataFun |
70 structure QuotData = Theory_Data |
72 (type T = quotient_info list |
71 (type T = quotient_info list |
73 val empty = [] |
72 val empty = [] |
74 val copy = I |
|
75 val extend = I |
73 val extend = I |
76 fun merge _ = (op @)) (* FIXME: is this the correct merging function for the list? *) |
74 val merge = (op @)) (* FIXME: is this the correct merging function for the list? *) |
77 |
75 |
78 val quotdata_lookup_thy = QuotData.get |
76 val quotdata_lookup_thy = QuotData.get |
79 val quotdata_lookup = QuotData.get o ProofContext.theory_of |
77 val quotdata_lookup = QuotData.get o ProofContext.theory_of |
80 |
78 |
81 fun quotdata_update_thy (qty, rty, rel, equiv_thm) thy = |
79 fun quotdata_update_thy (qty, rty, rel, equiv_thm) thy = |