# 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;