src/HOL/Ord.thy

--- a/src/HOL/Ord.thy	Fri Mar 17 22:46:26 1995 +0100
+++ b/src/HOL/Ord.thy	Mon Mar 20 15:35:28 1995 +0100
@@ -18,8 +18,8 @@
 
 defs
   mono_def      "mono(f) == (!A B. A <= B --> f(A) <= f(B))"
-  min_def       "min a b == if (a <= b) a b"
-  max_def       "max a b == if (a <= b) b a"
+  min_def       "min a b == (if a <= b then a else b)"
+  max_def       "max a b == (if a <= b then b else a)"
 
 end