# HG changeset patch
# User paulson
# Date 956135611 -7200
# Node ID 8a5b3f58b944079d17eb234d9037916732bdfd6f
# Parent  61bc5ed22b621c6ef63f5639eddc52868d7ea56a
deleted obsolete lemma_not_leI2

diff -r 61bc5ed22b62 -r 8a5b3f58b944 src/HOL/Real/RealOrd.ML
--- 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;