changeset 23139 | aa899bce7c3b |
parent 22144 | c33450acd873 |
child 24600 | 5877b88f262c |
23138:6852373aae8a | 23139:aa899bce7c3b |
---|---|
2 ID: $Id$ |
2 ID: $Id$ |
3 |
3 |
4 Compatibility wrapper for Poly/ML 5.0. |
4 Compatibility wrapper for Poly/ML 5.0. |
5 *) |
5 *) |
6 |
6 |
7 use "ML-Systems/polyml-4.1.4-patch.ML"; |
|
8 use "ML-Systems/polyml.ML"; |
7 use "ML-Systems/polyml.ML"; |
9 |
8 |
10 val pointer_eq = PolyML.pointerEq; |
9 val pointer_eq = PolyML.pointerEq; |
11 |
10 |
12 |
11 |