| changeset 35762 | af3ff2ba4c54 |
| parent 33522 | 737589bb9bb8 |
| child 36541 | de1862c4a308 |
| 35761:c4a698ee83b4 | 35762:af3ff2ba4c54 |
|---|---|
1 (* Title: ZF/Tools/ind_cases.ML |
1 (* Title: ZF/Tools/ind_cases.ML |
2 ID: $Id$ |
|
3 Author: Markus Wenzel, LMU Muenchen |
2 Author: Markus Wenzel, LMU Muenchen |
4 |
3 |
5 Generic inductive cases facility for (co)inductive definitions. |
4 Generic inductive cases facility for (co)inductive definitions. |
6 *) |
5 *) |
7 |
6 |