| changeset 28308 | d4396a28fb29 |
| parent 27691 | ce171cbd4b93 |
| child 28703 | aef727ef30e5 |
| 28307:39328b6ea7e8 | 28308:d4396a28fb29 |
|---|---|
1 (* Title: HOL/Tools/primrec_package.ML |
1 (* Title: HOL/Tools/old_primrec_package.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Stefan Berghofer, TU Muenchen and Norbert Voelker, FernUni Hagen |
3 Author: Stefan Berghofer, TU Muenchen and Norbert Voelker, FernUni Hagen |
4 |
4 |
5 Package for defining functions on datatypes by primitive recursion. |
5 Package for defining functions on datatypes by primitive recursion. |
6 *) |
6 *) |