# HG changeset patch
# User oheimb
# Date 829823585 -7200
# Node ID 1e2462c3fece9f30fb64abe6b902400da26ffc6e
# Parent  8cb42cd9757922f59c0ac1aadc88d19c1ba5e18b
*** empty log message ***

diff -r 8cb42cd97579 -r 1e2462c3fece src/FOL/ex/Nat2.ML
--- a/src/FOL/ex/Nat2.ML	Wed Apr 17 17:59:58 1996 +0200
+++ b/src/FOL/ex/Nat2.ML	Thu Apr 18 12:33:05 1996 +0200
@@ -158,6 +158,9 @@
 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 (ALL_IND_TAC nat_exh (asm_simp_tac nat_ss) 1);
+by (rtac nat_exh 1);
+by (simp_tac nat_ss 1);
+by (simp_tac nat_ss 1);
+by (asm_simp_tac nat_ss 1);
 qed "less_succ";