equal
deleted
inserted
replaced
9 uses |
9 uses |
10 "Tools/dseq.ML" |
10 "Tools/dseq.ML" |
11 ("Tools/inductive.ML") |
11 ("Tools/inductive.ML") |
12 ("Tools/Datatype/datatype_aux.ML") |
12 ("Tools/Datatype/datatype_aux.ML") |
13 ("Tools/Datatype/datatype_prop.ML") |
13 ("Tools/Datatype/datatype_prop.ML") |
14 ("Tools/Datatype/datatype_abs_proofs.ML") |
|
15 ("Tools/Datatype/datatype_data.ML") |
14 ("Tools/Datatype/datatype_data.ML") |
16 ("Tools/Datatype/datatype_case.ML") |
15 ("Tools/Datatype/datatype_case.ML") |
17 ("Tools/Datatype/rep_datatype.ML") |
16 ("Tools/Datatype/rep_datatype.ML") |
18 ("Tools/Datatype/datatype_codegen.ML") |
17 ("Tools/Datatype/datatype_codegen.ML") |
19 ("Tools/Datatype/primrec.ML") |
18 ("Tools/Datatype/primrec.ML") |
275 |
274 |
276 text {* Package setup. *} |
275 text {* Package setup. *} |
277 |
276 |
278 use "Tools/Datatype/datatype_aux.ML" |
277 use "Tools/Datatype/datatype_aux.ML" |
279 use "Tools/Datatype/datatype_prop.ML" |
278 use "Tools/Datatype/datatype_prop.ML" |
280 use "Tools/Datatype/datatype_abs_proofs.ML" |
|
281 use "Tools/Datatype/datatype_data.ML" setup Datatype_Data.setup |
279 use "Tools/Datatype/datatype_data.ML" setup Datatype_Data.setup |
282 use "Tools/Datatype/datatype_case.ML" setup Datatype_Case.setup |
280 use "Tools/Datatype/datatype_case.ML" setup Datatype_Case.setup |
283 use "Tools/Datatype/rep_datatype.ML" |
281 use "Tools/Datatype/rep_datatype.ML" |
284 use "Tools/Datatype/datatype_codegen.ML" setup Datatype_Codegen.setup |
282 use "Tools/Datatype/datatype_codegen.ML" setup Datatype_Codegen.setup |
285 use "Tools/Datatype/primrec.ML" |
283 use "Tools/Datatype/primrec.ML" |