| author | haftmann |
| Tue, 20 Mar 2007 15:52:41 +0100 | |
| changeset 22484 | 25dfebd7b4c8 |
| parent 21688 | e5287f12f1e1 |
| permissions | -rw-r--r-- |
(* Title: Pure/ML-Systems/polyml-5.0.ML ID: $Id$ Compatibility wrapper for Poly/ML 5.0 -- version for Isabelle2005. *) structure Posix = struct open Posix; structure IO = struct open IO; val mkReader = mkTextReader; val mkWriter = mkTextWriter; end; end; structure TextIO = struct open TextIO; fun inputLine is = Option.getOpt (TextIO.inputLine is, ""); end; structure Substring = struct open Substring; val all = full; end; use "ML-Systems/polyml.ML"; val pointer_eq = PolyML.pointerEq;