changeset 43084 | 946c8e171ffd |
parent 42361 | 23f352990944 |
child 45701 | 615da8b8d758 |
43083:df41a5762c3d | 43084:946c8e171ffd |
---|---|
1 (* Title: HOL/Tools/Function/size.ML |
1 (* Title: HOL/Tools/Function/size.ML |
2 Author: Stefan Berghofer, Florian Haftmann & Alexander Krauss, TU Muenchen |
2 Author: Stefan Berghofer, Florian Haftmann, TU Muenchen |
3 |
3 |
4 Size functions for datatypes. |
4 Size functions for datatypes. |
5 *) |
5 *) |
6 |
6 |
7 signature SIZE = |
7 signature SIZE = |