--- a/src/HOL/Ord.ML Mon Mar 20 18:24:11 2000 +0100
+++ b/src/HOL/Ord.ML Mon Mar 20 18:25:35 2000 +0100
@@ -164,10 +164,13 @@
by (blast_tac (claset() addIs [order_trans]) 1);
qed "le_max_iff_disj";
-qed_goal "le_maxI1" Ord.thy "(x::'a::linorder) <= max x y"
- (K [rtac (le_max_iff_disj RS iffD2) 1, rtac (order_refl RS disjI1) 1]);
-qed_goal "le_maxI2" Ord.thy "(y::'a::linorder) <= max x y"
- (K [rtac (le_max_iff_disj RS iffD2) 1, rtac (order_refl RS disjI2) 1]);
+Goal "(x::'a::linorder) <= max x y";
+by (simp_tac (simpset() addsimps [le_max_iff_disj]) 1);
+qed "le_maxI1";
+
+Goal "(y::'a::linorder) <= max x y";
+by (simp_tac (simpset() addsimps [le_max_iff_disj]) 1);
+qed "le_maxI2";
(*CANNOT use with AddSIs because blast_tac will give PROOF FAILED.*)
Goalw [max_def] "!!z::'a::linorder. (z < max x y) = (z < x | z < y)";