| changeset 8343 | fb604f0e5640 |
| parent 8303 | 5e7037409118 |
| child 8482 | bbc805ebc904 |
| 8342:289ad8062cb5 | 8343:fb604f0e5640 |
|---|---|
1 (* Title: HOL/Inductive.thy |
1 (* Title: HOL/Inductive.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 *) |
3 *) |
4 |
4 |
5 theory Inductive = Gfp + Prod + Sum |
5 theory Inductive = Gfp + Prod + Sum + NatDef |
6 files |
6 files |
7 "Tools/induct_method.ML" |
7 "Tools/induct_method.ML" |
8 "Tools/inductive_package.ML" |
8 "Tools/inductive_package.ML" |
9 "Tools/datatype_aux.ML" |
9 "Tools/datatype_aux.ML" |
10 "Tools/datatype_prop.ML" |
10 "Tools/datatype_prop.ML" |