Now defines structure Int
authorpaulson
Fri, 01 Nov 1996 15:12:21 +0100
changeset 2141 c2aedd8169cd
parent 2140 eaa7ab39889d
child 2142 20f208ff085d
Now defines structure Int
src/Pure/NJ1xx.ML
src/Pure/POLY.ML
--- a/src/Pure/NJ1xx.ML	Wed Oct 30 11:21:24 1996 +0100
+++ b/src/Pure/NJ1xx.ML	Fri Nov 01 15:12:21 1996 +0100
@@ -14,6 +14,8 @@
   | exit _ = OS.Process.exit OS.Process.failure;
 fun quit () = exit 0;
 
+structure Int = Integer;
+
 (*To change the current directory*)
 val cd = OS.FileSys.chDir;
 
--- a/src/Pure/POLY.ML	Wed Oct 30 11:21:24 1996 +0100
+++ b/src/Pure/POLY.ML	Fri Nov 01 15:12:21 1996 +0100
@@ -9,6 +9,13 @@
 open PolyML ExtendedIO;
 
 
+structure Int =
+  struct
+  fun max (x, y) = if x < y then y else x : int;
+  fun min (x, y) = if x < y then x else y : int;
+  end;
+
+
 (*A conditional timing function: applies f to () and, if the flag is true,
   prints its runtime.*)