src/Pure/ML-Systems/polyml-4.2.0.ML
author haftmann
Mon, 16 Feb 2009 19:11:55 +0100
changeset 29940 83b373f61d41
parent 29564 f8b933a62151
child 30627 fb9e73c01603
permissions -rw-r--r--
more default simp rules for sgn
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
26215
94d32a7cd0fb rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML-Systems/polyml-4.2.0.ML
94d32a7cd0fb rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff changeset
     2
94d32a7cd0fb rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff changeset
     3
Compatibility wrapper for Poly/ML 4.2.0.
94d32a7cd0fb rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff changeset
     4
*)
94d32a7cd0fb rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff changeset
     5
28151
61f9c918b410 explicit use of universal.ML and dummy_thread.ML;
wenzelm
parents: 26377
diff changeset
     6
use "ML-Systems/universal.ML";
61f9c918b410 explicit use of universal.ML and dummy_thread.ML;
wenzelm
parents: 26377
diff changeset
     7
use "ML-Systems/thread_dummy.ML";
26215
94d32a7cd0fb rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
diff changeset
     8
use "ML-Systems/polyml_common.ML";
26377
54dc2f9c5be8 removed pointer_eq from polyml_common.ML (structure Address no longer available after 5.1);
wenzelm
parents: 26215
diff changeset
     9
use "ML-Systems/polyml_old_compiler4.ML";
54dc2f9c5be8 removed pointer_eq from polyml_common.ML (structure Address no longer available after 5.1);
wenzelm
parents: 26215
diff changeset
    10
54dc2f9c5be8 removed pointer_eq from polyml_common.ML (structure Address no longer available after 5.1);
wenzelm
parents: 26215
diff changeset
    11
val pointer_eq = Address.wordEq;
54dc2f9c5be8 removed pointer_eq from polyml_common.ML (structure Address no longer available after 5.1);
wenzelm
parents: 26215
diff changeset
    12