author | blanchet |
Wed, 12 Feb 2014 17:36:00 +0100 | |
changeset 55444 | ec73f81e49e7 |
parent 54900 | 136fe16e726a |
child 55763 | 4b3907cb5654 |
permissions | -rw-r--r-- |
33970 | 1 |
(* Title: HOL/Tools/Datatype/datatype_data.ML |
11539 | 2 |
Author: Stefan Berghofer, TU Muenchen |
5177 | 3 |
|
45890 | 4 |
Datatype package bookkeeping. |
5177 | 5 |
*) |
6 |
||
33970 | 7 |
signature DATATYPE_DATA = |
6360 | 8 |
sig |
33970 | 9 |
include DATATYPE_COMMON |
45890 | 10 |
val get_all : theory -> info Symtab.table |
33970 | 11 |
val get_info : theory -> string -> info option |
12 |
val the_info : theory -> string -> info |
|
45890 | 13 |
val info_of_constr : theory -> string * typ -> info option |
14 |
val info_of_constr_permissive : theory -> string * typ -> info option |
|
15 |
val info_of_case : theory -> string -> info option |
|
16 |
val register: (string * info) list -> theory -> theory |
|
17 |
val the_spec : theory -> string -> (string * sort) list * (string * typ list) list |
|
45701 | 18 |
val the_descr : theory -> string list -> |
19 |
descr * (string * sort) list * string list * string * |
|
20 |
(string list * string list) * (typ list * typ list) |
|
33970 | 21 |
val all_distincts : theory -> typ list -> thm list list |
22 |
val get_constrs : theory -> string -> (string * typ) list option |
|
45890 | 23 |
val mk_case_names_induct: descr -> attribute |
24 |
val mk_case_names_exhausts: descr -> string list -> attribute list |
|
33970 | 25 |
val interpretation : (config -> string list -> theory -> theory) -> theory -> theory |
45890 | 26 |
val interpretation_data : config * string list -> theory -> theory |
33970 | 27 |
val setup: theory -> theory |
32717
0e787c721fa3
re-established reasonable inner outline for module
haftmann
parents:
32712
diff
changeset
|
28 |
end; |
0e787c721fa3
re-established reasonable inner outline for module
haftmann
parents:
32712
diff
changeset
|
29 |
|
33970 | 30 |
structure Datatype_Data: DATATYPE_DATA = |
33963
977b94b64905
renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33959
diff
changeset
|
31 |
struct |
5177 | 32 |
|
33970 | 33 |
(** theory data **) |
34 |
||
35 |
(* data management *) |
|
36 |
||
45890 | 37 |
structure Data = Theory_Data |
33970 | 38 |
( |
39 |
type T = |
|
41423 | 40 |
{types: Datatype_Aux.info Symtab.table, |
41 |
constrs: (string * Datatype_Aux.info) list Symtab.table, |
|
42 |
cases: Datatype_Aux.info Symtab.table}; |
|
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
43 |
|
33970 | 44 |
val empty = |
45 |
{types = Symtab.empty, constrs = Symtab.empty, cases = Symtab.empty}; |
|
46 |
val extend = I; |
|
47 |
fun merge |
|
48 |
({types = types1, constrs = constrs1, cases = cases1}, |
|
49 |
{types = types2, constrs = constrs2, cases = cases2}) : T = |
|
50 |
{types = Symtab.merge (K true) (types1, types2), |
|
51 |
constrs = Symtab.join (K (AList.merge (op =) (K true))) (constrs1, constrs2), |
|
52 |
cases = Symtab.merge (K true) (cases1, cases2)}; |
|
53 |
); |
|
54 |
||
45890 | 55 |
val get_all = #types o Data.get; |
33970 | 56 |
val get_info = Symtab.lookup o get_all; |
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
57 |
|
33970 | 58 |
fun the_info thy name = |
59 |
(case get_info thy name of |
|
60 |
SOME info => info |
|
61 |
| NONE => error ("Unknown datatype " ^ quote name)); |
|
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
62 |
|
33970 | 63 |
fun info_of_constr thy (c, T) = |
64 |
let |
|
45890 | 65 |
val tab = Symtab.lookup_list (#constrs (Data.get thy)) c; |
43580
023a1d1f97bd
new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors -- side effect: function package correctly identifies 0::int as a non-constructor;
krauss
parents:
43329
diff
changeset
|
66 |
in |
45700 | 67 |
(case body_type T of |
43580
023a1d1f97bd
new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors -- side effect: function package correctly identifies 0::int as a non-constructor;
krauss
parents:
43329
diff
changeset
|
68 |
Type (tyco, _) => AList.lookup (op =) tab tyco |
45700 | 69 |
| _ => NONE) |
43580
023a1d1f97bd
new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors -- side effect: function package correctly identifies 0::int as a non-constructor;
krauss
parents:
43329
diff
changeset
|
70 |
end; |
023a1d1f97bd
new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors -- side effect: function package correctly identifies 0::int as a non-constructor;
krauss
parents:
43329
diff
changeset
|
71 |
|
023a1d1f97bd
new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors -- side effect: function package correctly identifies 0::int as a non-constructor;
krauss
parents:
43329
diff
changeset
|
72 |
fun info_of_constr_permissive thy (c, T) = |
023a1d1f97bd
new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors -- side effect: function package correctly identifies 0::int as a non-constructor;
krauss
parents:
43329
diff
changeset
|
73 |
let |
45890 | 74 |
val tab = Symtab.lookup_list (#constrs (Data.get thy)) c; |
45700 | 75 |
val hint = (case body_type T of Type (tyco, _) => SOME tyco | _ => NONE); |
76 |
val default = if null tab then NONE else SOME (snd (List.last tab)); |
|
77 |
(*conservative wrt. overloaded constructors*) |
|
78 |
in |
|
79 |
(case hint of |
|
80 |
NONE => default |
|
81 |
| SOME tyco => |
|
82 |
(case AList.lookup (op =) tab tyco of |
|
83 |
NONE => default (*permissive*) |
|
84 |
| SOME info => SOME info)) |
|
33970 | 85 |
end; |
86 |
||
45890 | 87 |
val info_of_case = Symtab.lookup o #cases o Data.get; |
33970 | 88 |
|
54400 | 89 |
fun ctrs_of_exhaust exhaust = |
90 |
Logic.strip_imp_prems (prop_of exhaust) |> |
|
91 |
map (head_of o snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o the_single |
|
92 |
o Logic.strip_assums_hyp); |
|
93 |
||
94 |
fun case_of_case_rewrite case_rewrite = |
|
95 |
head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of case_rewrite)))); |
|
96 |
||
97 |
fun ctr_sugar_of_info ({exhaust, nchotomy, inject, distinct, case_rewrites, case_cong, |
|
98 |
weak_case_cong, split, split_asm, ...} : Datatype_Aux.info) = |
|
99 |
{ctrs = ctrs_of_exhaust exhaust, |
|
100 |
casex = case_of_case_rewrite (hd case_rewrites), |
|
101 |
discs = [], |
|
102 |
selss = [], |
|
103 |
exhaust = exhaust, |
|
104 |
nchotomy = nchotomy, |
|
105 |
injects = inject, |
|
106 |
distincts = distinct, |
|
107 |
case_thms = case_rewrites, |
|
108 |
case_cong = case_cong, |
|
109 |
weak_case_cong = weak_case_cong, |
|
110 |
split = split, |
|
111 |
split_asm = split_asm, |
|
112 |
disc_thmss = [], |
|
113 |
discIs = [], |
|
114 |
sel_thmss = [], |
|
54900 | 115 |
disc_excludesss = [], |
54400 | 116 |
disc_exhausts = [], |
117 |
sel_exhausts = [], |
|
118 |
collapses = [], |
|
119 |
expands = [], |
|
120 |
sel_splits = [], |
|
121 |
sel_split_asms = [], |
|
54491 | 122 |
case_eq_ifs = []}; |
54400 | 123 |
|
124 |
fun register dt_infos = |
|
45890 | 125 |
Data.map (fn {types, constrs, cases} => |
33970 | 126 |
{types = types |> fold Symtab.update dt_infos, |
127 |
constrs = constrs |> fold (fn (constr, dtname_info) => |
|
128 |
Symtab.map_default (constr, []) (cons dtname_info)) |
|
129 |
(maps (fn (dtname, info as {descr, index, ...}) => |
|
54400 | 130 |
map (rpair (dtname, info) o fst) (#3 (the (AList.lookup op = descr index)))) dt_infos), |
33970 | 131 |
cases = cases |> fold Symtab.update |
54400 | 132 |
(map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)}) #> |
55444
ec73f81e49e7
iteration n in the 'default' vs. 'update_new' vs. 'update' saga -- 'update' makes sense now that we honor the canonical order on 'merge' (as opposed to raising 'DUP')
blanchet
parents:
54900
diff
changeset
|
133 |
fold (fn (key, info) => |
ec73f81e49e7
iteration n in the 'default' vs. 'update_new' vs. 'update' saga -- 'update' makes sense now that we honor the canonical order on 'merge' (as opposed to raising 'DUP')
blanchet
parents:
54900
diff
changeset
|
134 |
Ctr_Sugar.default_register_ctr_sugar_global key (ctr_sugar_of_info info)) dt_infos; |
33970 | 135 |
|
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
136 |
|
33970 | 137 |
(* complex queries *) |
138 |
||
139 |
fun the_spec thy dtco = |
|
140 |
let |
|
45822 | 141 |
val {descr, index, ...} = the_info thy dtco; |
45821 | 142 |
val (_, dtys, raw_cos) = the (AList.lookup (op =) descr index); |
45822 | 143 |
val args = map Datatype_Aux.dest_DtTFree dtys; |
144 |
val cos = map (fn (co, tys) => (co, map (Datatype_Aux.typ_of_dtyp descr) tys)) raw_cos; |
|
145 |
in (args, cos) end; |
|
33970 | 146 |
|
147 |
fun the_descr thy (raw_tycos as raw_tyco :: _) = |
|
148 |
let |
|
149 |
val info = the_info thy raw_tyco; |
|
150 |
val descr = #descr info; |
|
151 |
||
45822 | 152 |
val (_, dtys, _) = the (AList.lookup (op =) descr (#index info)); |
153 |
val vs = map Datatype_Aux.dest_DtTFree dtys; |
|
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
154 |
|
41423 | 155 |
fun is_DtTFree (Datatype_Aux.DtTFree _) = true |
45700 | 156 |
| is_DtTFree _ = false; |
33970 | 157 |
val k = find_index (fn (_, (_, dTs, _)) => not (forall is_DtTFree dTs)) descr; |
41423 | 158 |
val protoTs as (dataTs, _) = |
159 |
chop k descr |
|
160 |
|> (pairself o map) |
|
45822 | 161 |
(fn (_, (tyco, dTs, _)) => (tyco, map (Datatype_Aux.typ_of_dtyp descr) dTs)); |
45700 | 162 |
|
33970 | 163 |
val tycos = map fst dataTs; |
45430 | 164 |
val _ = |
165 |
if eq_set (op =) (tycos, raw_tycos) then () |
|
45700 | 166 |
else |
167 |
error ("Type constructors " ^ commas_quote raw_tycos ^ |
|
168 |
" do not belong exhaustively to one mutual recursive datatype"); |
|
33970 | 169 |
|
170 |
val (Ts, Us) = (pairself o map) Type protoTs; |
|
171 |
||
45701 | 172 |
val names = map Long_Name.base_name tycos; |
45700 | 173 |
val (auxnames, _) = |
174 |
Name.make_context names |
|
43326
47cf4bc789aa
simplified Name.variant -- discontinued builtin fold_map;
wenzelm
parents:
43253
diff
changeset
|
175 |
|> fold_map (Name.variant o Datatype_Aux.name_of_typ) Us; |
33970 | 176 |
val prefix = space_implode "_" names; |
177 |
||
178 |
in (descr, vs, tycos, prefix, (names, auxnames), (Ts, Us)) end; |
|
179 |
||
180 |
fun all_distincts thy Ts = |
|
181 |
let |
|
182 |
fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts |
|
183 |
| add_tycos _ = I; |
|
184 |
val tycos = fold add_tycos Ts []; |
|
185 |
in map_filter (Option.map #distinct o get_info thy) tycos end; |
|
186 |
||
187 |
fun get_constrs thy dtco = |
|
45700 | 188 |
(case try (the_spec thy) dtco of |
45822 | 189 |
SOME (args, cos) => |
45700 | 190 |
let |
191 |
fun subst (v, sort) = TVar ((v, 0), sort); |
|
192 |
fun subst_ty (TFree v) = subst v |
|
193 |
| subst_ty ty = ty; |
|
45822 | 194 |
val dty = Type (dtco, map subst args); |
45700 | 195 |
fun mk_co (co, tys) = (co, map (Term.map_atyps subst_ty) tys ---> dty); |
196 |
in SOME (map mk_co cos) end |
|
197 |
| NONE => NONE); |
|
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
198 |
|
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
199 |
|
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
200 |
|
33970 | 201 |
(** various auxiliary **) |
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
202 |
|
33970 | 203 |
(* case names *) |
204 |
||
205 |
local |
|
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
206 |
|
41423 | 207 |
fun dt_recs (Datatype_Aux.DtTFree _) = [] |
208 |
| dt_recs (Datatype_Aux.DtType (_, dts)) = maps dt_recs dts |
|
209 |
| dt_recs (Datatype_Aux.DtRec i) = [i]; |
|
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
210 |
|
41423 | 211 |
fun dt_cases (descr: Datatype_Aux.descr) (_, args, constrs) = |
33970 | 212 |
let |
213 |
fun the_bname i = Long_Name.base_name (#1 (the (AList.lookup (op =) descr i))); |
|
214 |
val bnames = map the_bname (distinct (op =) (maps dt_recs args)); |
|
215 |
in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end; |
|
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
216 |
|
33970 | 217 |
fun induct_cases descr = |
218 |
Datatype_Prop.indexify_names (maps (dt_cases descr) (map #2 descr)); |
|
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
219 |
|
33970 | 220 |
fun exhaust_cases descr i = dt_cases descr (the (AList.lookup (op =) descr i)); |
221 |
||
222 |
in |
|
223 |
||
224 |
fun mk_case_names_induct descr = Rule_Cases.case_names (induct_cases descr); |
|
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
225 |
|
33970 | 226 |
fun mk_case_names_exhausts descr new = |
227 |
map (Rule_Cases.case_names o exhaust_cases descr o #1) |
|
228 |
(filter (fn ((_, (name, _, _))) => member (op =) new name) descr); |
|
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
229 |
|
33970 | 230 |
end; |
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
231 |
|
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
232 |
|
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
233 |
|
33970 | 234 |
(** document antiquotation **) |
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
235 |
|
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
236 |
val antiq_setup = |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
237 |
Thy_Output.antiquotation @{binding datatype} (Args.type_name true) |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
238 |
(fn {source = src, context = ctxt, ...} => fn dtco => |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
239 |
let |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
240 |
val thy = Proof_Context.theory_of ctxt; |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
241 |
val (vs, cos) = the_spec thy dtco; |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
242 |
val ty = Type (dtco, map TFree vs); |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
243 |
val pretty_typ_bracket = Syntax.pretty_typ (Config.put pretty_priority 1001 ctxt); |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
244 |
fun pretty_constr (co, tys) = |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
245 |
Pretty.block (Pretty.breaks |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
246 |
(Syntax.pretty_term ctxt (Const (co, tys ---> ty)) :: |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
247 |
map pretty_typ_bracket tys)); |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
248 |
val pretty_datatype = |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
249 |
Pretty.block |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
250 |
(Pretty.command "datatype" :: Pretty.brk 1 :: |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
251 |
Syntax.pretty_typ ctxt ty :: |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
252 |
Pretty.str " =" :: Pretty.brk 1 :: |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
253 |
flat (separate [Pretty.brk 1, Pretty.str "| "] (map (single o pretty_constr) cos))); |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
254 |
in |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
255 |
Thy_Output.output ctxt |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
256 |
(Thy_Output.maybe_pretty_source (K (K pretty_datatype)) ctxt src [()]) |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
257 |
end); |
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
258 |
|
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
259 |
|
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
260 |
|
33970 | 261 |
(** abstract theory extensions relative to a datatype characterisation **) |
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
262 |
|
33970 | 263 |
structure Datatype_Interpretation = Interpretation |
45700 | 264 |
( |
265 |
type T = Datatype_Aux.config * string list; |
|
266 |
val eq: T * T -> bool = eq_snd (op =); |
|
267 |
); |
|
33970 | 268 |
fun interpretation f = Datatype_Interpretation.interpretation (uncurry f); |
45890 | 269 |
val interpretation_data = Datatype_Interpretation.data; |
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
270 |
|
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
271 |
|
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset
|
272 |
|
45890 | 273 |
(** setup theory **) |
33970 | 274 |
|
275 |
val setup = |
|
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43329
diff
changeset
|
276 |
antiq_setup #> |
33970 | 277 |
Datatype_Interpretation.init; |
278 |
||
41423 | 279 |
open Datatype_Aux; |
280 |
||
30391
d930432adb13
adapted to simplified ThyOutput.antiquotation interface;
wenzelm
parents:
30364
diff
changeset
|
281 |
end; |