--- a/src/HOL/Ord.ML Sun Sep 26 16:46:25 1999 +0200
+++ b/src/HOL/Ord.ML Mon Sep 27 10:25:10 1999 +0200
@@ -158,7 +158,7 @@
(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]);
-AddSIs[le_maxI1, 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)";
by (simp_tac (simpset() addsimps [order_le_less]) 1);