deleted obsolete lemma_not_leI2

--- a/src/HOL/Real/RealOrd.ML	Wed Apr 19 11:09:59 2000 +0200
+++ b/src/HOL/Real/RealOrd.ML	Wed Apr 19 11:13:31 2000 +0200
@@ -791,10 +791,6 @@
 by (blast_tac (claset() addDs [less_le_trans] addIs [less_asym]) 1);
 qed "lemma_not_leI";
 
-Goalw [le_def] "!!m. ~ Suc n <= m ==> ~ Suc (Suc n) <= m";
-by Auto_tac;
-qed "lemma_not_leI2";
-
 (*------- lemmas -------*)
 context Arith.thy;