src/HOL/IOA/NTP/Lemmas.ML

--- a/src/HOL/IOA/NTP/Lemmas.ML	Thu Sep 12 10:36:51 1996 +0200
+++ b/src/HOL/IOA/NTP/Lemmas.ML	Thu Sep 12 10:40:05 1996 +0200
@@ -156,10 +156,7 @@
 
 goal Arith.thy "~0<n --> n = 0";
   by (nat_ind_tac "n" 1);
-  by (Asm_simp_tac 1);
-  by (safe_tac (!claset));
-  by (Asm_full_simp_tac 1);
-  by (Asm_full_simp_tac 1);
+  by (Auto_tac ());
 qed "zero_eq";
 
 goal Arith.thy "x < Suc(y) --> x<=y";