src/HOL/Hyperreal/SEQ.ML

--- a/src/HOL/Hyperreal/SEQ.ML	Tue Nov 25 10:37:03 2003 +0100
+++ b/src/HOL/Hyperreal/SEQ.ML	Thu Nov 27 10:47:55 2003 +0100
@@ -661,7 +661,7 @@
 by (dtac lemma_converg3 1);
 by (dtac isLub_le_isUb 1 THEN assume_tac 1);
 by (auto_tac (claset() addDs [order_less_le_trans],
-              simpset() addsimps [real_minus_zero_le_iff]));
+              simpset()));
 val lemma_converg4 = result();
 
 (*-------------------------------------------------------------------