# HG changeset patch
# User oheimb
# Date 829829462 -7200
# Node ID a6b55b9d2f2219f06e5278f0627d79a6c03b898b
# Parent  1e2462c3fece9f30fb64abe6b902400da26ffc6e
adapted proof of less_succ: problem because of non-confluent SimpSet removed

diff -r 1e2462c3fece -r a6b55b9d2f22 src/FOL/ex/Nat2.ML
--- a/src/FOL/ex/Nat2.ML	Thu Apr 18 12:33:05 1996 +0200
+++ b/src/FOL/ex/Nat2.ML	Thu Apr 18 14:11:02 1996 +0200
@@ -158,9 +158,7 @@
 by (IND_TAC nat_ind (simp_tac nat_ss) "j" 1);
 by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1);
 by (resolve_tac [impI RS allI] 1);
-by (rtac nat_exh 1);
-by (simp_tac nat_ss 1);
-by (simp_tac nat_ss 1);
+by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1);
 by (asm_simp_tac nat_ss 1);
 qed "less_succ";