equal
deleted
inserted
replaced
9 |
9 |
10 theory Datatype |
10 theory Datatype |
11 imports Product_Type Sum_Type Nat |
11 imports Product_Type Sum_Type Nat |
12 uses |
12 uses |
13 ("Tools/Datatype/datatype_rep_proofs.ML") |
13 ("Tools/Datatype/datatype_rep_proofs.ML") |
|
14 ("Tools/Datatype/datatype.ML") |
14 ("Tools/inductive_realizer.ML") |
15 ("Tools/inductive_realizer.ML") |
15 ("Tools/Datatype/datatype_realizer.ML") |
16 ("Tools/Datatype/datatype_realizer.ML") |
16 begin |
17 begin |
17 |
18 |
18 subsection {* The datatype universe *} |
19 subsection {* The datatype universe *} |
518 text {* hides popular names *} |
519 text {* hides popular names *} |
519 hide (open) type node item |
520 hide (open) type node item |
520 hide (open) const Push Node Atom Leaf Numb Lim Split Case |
521 hide (open) const Push Node Atom Leaf Numb Lim Split Case |
521 |
522 |
522 use "Tools/Datatype/datatype_rep_proofs.ML" |
523 use "Tools/Datatype/datatype_rep_proofs.ML" |
|
524 use "Tools/Datatype/datatype.ML" |
523 |
525 |
524 use "Tools/inductive_realizer.ML" |
526 use "Tools/inductive_realizer.ML" |
525 setup InductiveRealizer.setup |
527 setup InductiveRealizer.setup |
526 |
528 |
527 use "Tools/Datatype/datatype_realizer.ML" |
529 use "Tools/Datatype/datatype_realizer.ML" |