tuned;

--- a/src/FOL/ex/Natural_Numbers.thy	Fri Oct 12 12:06:10 2001 +0200
+++ b/src/FOL/ex/Natural_Numbers.thy	Fri Oct 12 12:06:23 2001 +0200
@@ -62,8 +62,8 @@
 
 lemma "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i + j) = i + f(j)"
 proof -
-  assume a: "!!n. f(Suc(n)) = Suc(f(n))"
-  show ?thesis by (induct i) (simp, simp add: a)  (* FIXME tune *)
+  assume "!!n. f(Suc(n)) = Suc(f(n))"
+  thus ?thesis by (induct i) simp_all
 qed
 
 end