author | wenzelm |
Thu, 22 Nov 2007 14:51:34 +0100 | |
changeset 25456 | 6f79698f294d |
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;