equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 header {* Support for inductive sets and types *} |
6 header {* Support for inductive sets and types *} |
7 |
7 |
8 theory Inductive |
8 theory Inductive |
9 imports FixedPoint Sum_Type Relation Record |
9 imports FixedPoint Product_Type Sum_Type |
10 uses |
10 uses |
11 ("Tools/inductive_package.ML") |
11 ("Tools/inductive_package.ML") |
12 ("Tools/old_inductive_package.ML") |
12 ("Tools/old_inductive_package.ML") |
13 ("Tools/inductive_realizer.ML") |
13 ("Tools/inductive_realizer.ML") |
14 ("Tools/inductive_codegen.ML") |
14 ("Tools/inductive_codegen.ML") |