src/Pure/General/integer.ML

--- a/src/Pure/General/integer.ML	Tue Oct 20 20:03:23 2009 +0200
+++ b/src/Pure/General/integer.ML	Tue Oct 20 20:54:31 2009 +0200
@@ -6,6 +6,8 @@
 
 signature INTEGER =
 sig
+  val min: int -> int -> int
+  val max: int -> int -> int
   val add: int -> int -> int
   val mult: int -> int -> int
   val sum: int list -> int
@@ -23,6 +25,9 @@
 structure Integer : INTEGER =
 struct
 
+fun min x y = Int.min (x, y);
+fun max x y = Int.max (x, y);
+
 fun add x y = x + y;
 fun mult x y = x * y;