*** empty log message ***

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