equal
deleted
inserted
replaced
2 ID: $Id$ |
2 ID: $Id$ |
3 *) |
3 *) |
4 |
4 |
5 theory Inductive = Gfp + Prod + Sum |
5 theory Inductive = Gfp + Prod + Sum |
6 files |
6 files |
|
7 "Tools/induct_method.ML" |
7 "Tools/inductive_package.ML" |
8 "Tools/inductive_package.ML" |
8 "Tools/datatype_aux.ML" |
9 "Tools/datatype_aux.ML" |
9 "Tools/datatype_prop.ML" |
10 "Tools/datatype_prop.ML" |
10 "Tools/datatype_rep_proofs.ML" |
11 "Tools/datatype_rep_proofs.ML" |
11 "Tools/datatype_abs_proofs.ML" |
12 "Tools/datatype_abs_proofs.ML" |
12 "Tools/datatype_package.ML" |
13 "Tools/datatype_package.ML" |
13 "Tools/primrec_package.ML": |
14 "Tools/primrec_package.ML": |
14 |
15 |
|
16 setup InductMethod.setup |
15 setup InductivePackage.setup |
17 setup InductivePackage.setup |
16 setup DatatypePackage.setup |
18 setup DatatypePackage.setup |
17 |
19 |
18 theorems [mono] = |
20 theorems [mono] = |
19 subset_refl imp_refl disj_mono conj_mono ex_mono all_mono |
21 subset_refl imp_refl disj_mono conj_mono ex_mono all_mono |