| changeset 28255 | 6faea8ad8559 |
| parent 25733 | 8722d68471ff |
| child 29564 | f8b933a62151 |
| 28254:d67ba23e0277 | 28255:6faea8ad8559 |
|---|---|
1 (* Title: Pure/ML-Systems/universal.ML |
1 (* Title: Pure/ML-Systems/universal.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Makarius |
3 Author: Makarius |
4 |
4 |
5 Universal values via tagged union. Emulates structure Universal |
5 Universal values via tagged union. Emulates structure Universal |
6 in Poly/ML 5.1. |
6 from Poly/ML 5.1. |
7 *) |
7 *) |
8 |
8 |
9 signature UNIVERSAL = |
9 signature UNIVERSAL = |
10 sig |
10 sig |
11 type universal |
11 type universal |