src/Pure/ML-Systems/polyml-5.0.ML
author wenzelm
Tue, 05 Dec 2006 18:33:29 +0100
changeset 21653 219924615db6
child 21771 148c8aba89dd
permissions -rw-r--r--
setup for polyml-5.0;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
21653
219924615db6 setup for polyml-5.0;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML-Systems/polyml-5.0.ML
219924615db6 setup for polyml-5.0;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
219924615db6 setup for polyml-5.0;
wenzelm
parents:
diff changeset
     3
219924615db6 setup for polyml-5.0;
wenzelm
parents:
diff changeset
     4
Compatibility wrapper for Poly/ML 5.0.
219924615db6 setup for polyml-5.0;
wenzelm
parents:
diff changeset
     5
*)
219924615db6 setup for polyml-5.0;
wenzelm
parents:
diff changeset
     6
219924615db6 setup for polyml-5.0;
wenzelm
parents:
diff changeset
     7
use "ML-Systems/polyml-4.1.4-patch.ML";
219924615db6 setup for polyml-5.0;
wenzelm
parents:
diff changeset
     8
use "ML-Systems/polyml.ML";
219924615db6 setup for polyml-5.0;
wenzelm
parents:
diff changeset
     9
219924615db6 setup for polyml-5.0;
wenzelm
parents:
diff changeset
    10
val pointer_eq = PolyML.pointerEq;