changeset 29564 | f8b933a62151 |
parent 28490 | 40c3f900c457 |
child 32566 | e6b66a59bed6 |
29563:4773c5c994dc | 29564:f8b933a62151 |
---|---|
1 (* Title: Pure/ML-Systems/proper_int.ML |
1 (* Title: Pure/ML-Systems/proper_int.ML |
2 ID: $Id$ |
|
3 Author: Makarius |
2 Author: Makarius |
4 |
3 |
5 SML basis with type int representing proper integers, not machine |
4 SML basis with type int representing proper integers, not machine |
6 words. |
5 words. |
7 *) |
6 *) |