src/Pure/ML-Systems/polyml-4.1.4.ML
author wenzelm
Mon, 24 Sep 2007 13:52:50 +0200
changeset 24688 a5754ca5c510
parent 23139 aa899bce7c3b
child 26215 94d32a7cd0fb
permissions -rw-r--r--
replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23139
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML-Systems/polyml-4.1.4.ML
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
     3
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
     4
Compatibility wrapper for Poly/ML 4.1.4.
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
     5
*)
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
     6
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
     7
use "ML-Systems/polyml-old-basis.ML";
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
     8
use "ML-Systems/polyml.ML";