--- a/src/HOL/Orderings.thy Mon May 01 18:10:18 2006 +0200
+++ b/src/HOL/Orderings.thy Mon May 01 18:10:40 2006 +0200
@@ -68,14 +68,14 @@
by (simp add: min_def)
lemma min_of_mono:
- "ALL x y. (f x <= f y) = (x <= y) ==> min (f m) (f n) = f (min m n)"
+ "(!!x y. (f x <= f y) = (x <= y)) ==> min (f m) (f n) = f (min m n)"
by (simp add: min_def)
lemma max_leastL: "(!!x. least <= x) ==> max least x = x"
by (simp add: max_def)
lemma max_of_mono:
- "ALL x y. (f x <= f y) = (x <= y) ==> max (f m) (f n) = f (max m n)"
+ "(!!x y. (f x <= f y) = (x <= y)) ==> max (f m) (f n) = f (max m n)"
by (simp add: max_def)