# HG changeset patch
# User paulson
# Date 1021646844 -7200
# Node ID eca781285662042b11b1f5886c6d09d3158382b6
# Parent  2af7b94892ce411f0bb783ef841f0becfa271d44
deleting the obsolete theorem lt_succ_iff

diff -r 2af7b94892ce -r eca781285662 src/ZF/Arith.ML
--- a/src/ZF/Arith.ML	Fri May 17 15:40:59 2002 +0200
+++ b/src/ZF/Arith.ML	Fri May 17 16:47:24 2002 +0200
@@ -509,14 +509,6 @@
 by Auto_tac;
 qed "lt_succ_eq_0_disj";
 
-Goal "[| m:nat; n:nat |] ==> (m < succ(n)) <-> (m < n | m =n)";
-by (induct_tac "n" 1);
-by (auto_tac (claset() addIs [leI], simpset()));
-by (dtac not_lt_imp_le 1);
-by Auto_tac;
-by (auto_tac (claset(), simpset() addsimps [le_iff]));
-qed "lt_succ_iff";
-
 Goal "[| j:nat; k:nat |] ==> ALL i:nat. (i < j #- k) <-> (i #+ k < j)";
 by (eres_inst_tac [("m", "k")] diff_induct  1);
 by Auto_tac;
diff -r 2af7b94892ce -r eca781285662 src/ZF/List.ML
--- a/src/ZF/List.ML	Fri May 17 15:40:59 2002 +0200
+++ b/src/ZF/List.ML	Fri May 17 16:47:24 2002 +0200
@@ -1133,11 +1133,10 @@
 qed "length_upt";
 Addsimps [length_upt];
 
-Goal "[| i:nat; j:nat; k:nat |] ==> \
-\ i #+ k < j --> nth(k, upt(i,j)) = i #+ k";
+Goal "[| i:nat; j:nat; k:nat |] ==> i #+ k < j --> nth(k, upt(i,j)) = i #+ k";
 by (induct_tac "j" 1);
 by (Asm_simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [nth_append,lt_succ_iff] 
+by (asm_full_simp_tac (simpset() addsimps [nth_append,le_iff] 
                                  addsplits [nat_diff_split]) 1);
 by Safe_tac;
 by (auto_tac (claset() addSDs [not_lt_imp_le],