equal
deleted
inserted
replaced
5 header {* Knaster-Tarski Fixpoint Theorem and inductive definitions *} |
5 header {* Knaster-Tarski Fixpoint Theorem and inductive definitions *} |
6 |
6 |
7 theory Inductive |
7 theory Inductive |
8 imports Complete_Lattices |
8 imports Complete_Lattices |
9 uses |
9 uses |
|
10 "Tools/dseq.ML" |
10 ("Tools/inductive.ML") |
11 ("Tools/inductive.ML") |
11 "Tools/dseq.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") |
14 ("Tools/Datatype/datatype_abs_proofs.ML") |
15 ("Tools/Datatype/datatype_data.ML") |
15 ("Tools/Datatype/datatype_data.ML") |
16 ("Tools/Datatype/datatype_case.ML") |
16 ("Tools/Datatype/datatype_case.ML") |
17 ("Tools/Datatype/rep_datatype.ML") |
17 ("Tools/Datatype/rep_datatype.ML") |
18 ("Tools/primrec.ML") |
|
19 ("Tools/Datatype/datatype_codegen.ML") |
18 ("Tools/Datatype/datatype_codegen.ML") |
|
19 ("Tools/Datatype/primrec.ML") |
20 begin |
20 begin |
21 |
21 |
22 subsection {* Least and greatest fixed points *} |
22 subsection {* Least and greatest fixed points *} |
23 |
23 |
24 context complete_lattice |
24 context complete_lattice |
274 |
274 |
275 subsection {* Inductive datatypes and primitive recursion *} |
275 subsection {* Inductive datatypes and primitive recursion *} |
276 |
276 |
277 text {* Package setup. *} |
277 text {* Package setup. *} |
278 |
278 |
|
279 use "Tools/Datatype/datatype_aux.ML" |
|
280 use "Tools/Datatype/datatype_prop.ML" |
279 use "Tools/Datatype/datatype_abs_proofs.ML" |
281 use "Tools/Datatype/datatype_abs_proofs.ML" |
280 use "Tools/Datatype/datatype_data.ML" setup Datatype_Data.setup |
282 use "Tools/Datatype/datatype_data.ML" setup Datatype_Data.setup |
281 use "Tools/Datatype/datatype_case.ML" setup Datatype_Case.setup |
283 use "Tools/Datatype/datatype_case.ML" setup Datatype_Case.setup |
282 use "Tools/Datatype/rep_datatype.ML" |
284 use "Tools/Datatype/rep_datatype.ML" |
283 |
285 use "Tools/Datatype/datatype_codegen.ML" setup Datatype_Codegen.setup |
284 use "Tools/Datatype/datatype_codegen.ML" |
286 use "Tools/Datatype/primrec.ML" |
285 setup Datatype_Codegen.setup |
|
286 |
|
287 use "Tools/primrec.ML" |
|
288 |
287 |
289 text{* Lambda-abstractions with pattern matching: *} |
288 text{* Lambda-abstractions with pattern matching: *} |
290 |
289 |
291 syntax |
290 syntax |
292 "_lam_pats_syntax" :: "cases_syn => 'a => 'b" ("(%_)" 10) |
291 "_lam_pats_syntax" :: "cases_syn => 'a => 'b" ("(%_)" 10) |