equal
deleted
inserted
replaced
1 (* Title: Pure/ML-Systems/polyml-4.9.1.ML |
|
2 ID: $Id$ |
|
3 |
|
4 Compatibility wrapper for Poly/ML 4.9.1. |
|
5 *) |
|
6 |
|
7 use "ML-Systems/polyml-4.1.4-patch.ML"; |
|
8 use "ML-Systems/polyml.ML"; |
|
9 |
|
10 val pointer_eq = PolyML.pointerEq; |
|