| changeset 11726 | 2b2a45abe876 |
| parent 11696 | 233362cfecc7 |
| child 11789 | da81334357ba |
--- 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