equal
deleted
inserted
replaced
43 |
43 |
44 val maps_lookup = Symtab.lookup o MapsData.get |
44 val maps_lookup = Symtab.lookup o MapsData.get |
45 |
45 |
46 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo)) |
46 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo)) |
47 fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo) |
47 fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo) |
48 (* FIXME: this should be done using a generic context *) |
|
49 |
48 |
50 fun maps_attribute_aux s minfo = Thm.declaration_attribute |
49 fun maps_attribute_aux s minfo = Thm.declaration_attribute |
51 (fn thm => Context.mapping (maps_update_thy s minfo) (maps_update s minfo)) |
50 (fn thm => Context.mapping (maps_update_thy s minfo) (maps_update s minfo)) |
52 |
51 |
53 (* attribute to be used in declare statements *) |
52 (* attribute to be used in declare statements *) |
70 val _ = Context.>> (Context.map_theory |
69 val _ = Context.>> (Context.map_theory |
71 (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) |
70 (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) |
72 "declaration of map information")) |
71 "declaration of map information")) |
73 |
72 |
74 |
73 |
75 (* info about the quotient types *) |
74 (* info about quotient types *) |
76 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} |
75 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} |
77 |
76 |
78 structure QuotData = Theory_Data |
77 structure QuotData = Theory_Data |
79 (type T = quotient_info Symtab.table |
78 (type T = quotient_info Symtab.table |
80 val empty = Symtab.empty |
79 val empty = Symtab.empty |
115 val _ = |
114 val _ = |
116 OuterSyntax.improper_command "print_quotients" "print out all quotients" |
115 OuterSyntax.improper_command "print_quotients" "print out all quotients" |
117 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of))) |
116 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of))) |
118 |
117 |
119 |
118 |
120 (* environments of quotient and raw types *) |
119 (* FIXME: obsolete: environments for quotient and raw types *) |
121 type qenv = (typ * typ) list |
120 type qenv = (typ * typ) list |
122 |
121 |
123 fun mk_qenv ctxt = |
122 fun mk_qenv ctxt = |
124 let |
123 let |
125 val thy = ProofContext.theory_of ctxt |
124 val thy = ProofContext.theory_of ctxt |