| changeset 53609 | 0f472e7063af |
| parent 53603 | 59ef06cda7b9 |
| child 53610 | dde3cc2804cc |
| 53608:53bd62921c54 | 53609:0f472e7063af |
|---|---|
1 (* Title: HOL/Tools/Function/fun_cases.ML |
1 (* Title: HOL/Tools/Function/fun_cases.ML |
2 Author: Manuel Eberl <eberlm@in.tum.de>, TU München |
2 Author: Manuel Eberl, TU Muenchen |
3 |
3 |
4 Provides the fun_cases command for generating specialised elimination |
4 Provides the fun_cases command for generating specialised elimination |
5 rules for function package functions. |
5 rules for function package functions. |
6 *) |
6 *) |
7 |
7 |