# HG changeset patch
# User paulson
# Date 938420710 -7200
# Node ID e783adccf39e9524b14ad4a4742cc684e53fb81c
# Parent  f677cdc7fae9cbc8153e07b4fd7ada4ab33a8a9d
removed order-sorted theorems from the default claset

diff -r f677cdc7fae9 -r e783adccf39e src/HOL/Ord.ML
--- 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);