src/Pure/POLY.ML
changeset 2141 c2aedd8169cd
parent 1480 85ecd3439e01
child 2242 fa8c6c695a97
--- 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.*)