| changeset 23921 | 947152add153 |
| parent 23826 | 463903573934 |
| child 23965 | f93e509659c1 |
| 23920:4288dc7dc248 | 23921:947152add153 |
|---|---|
1 (* Title: Pure/ML-Systems/polyml.ML |
1 (* Title: Pure/ML-Systems/polyml.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 |
3 |
4 Compatibility file for Poly/ML (version 4.1.x and 4.2.0). |
4 Compatibility file for Poly/ML (version 4.1.x and 4.2.0). |
5 *) |
5 *) |
6 |
|
7 use "ML-Systems/no_multithreading.ML"; |
|
8 |
|
6 |
9 |
7 (** ML system and platform related **) |
10 (** ML system and platform related **) |
8 |
11 |
9 (* String compatibility *) |
12 (* String compatibility *) |
10 |
13 |