tuned;
authorwenzelm
Fri Oct 12 12:06:23 2001 +0200 (2001-10-12)
changeset 117262b2a45abe876
parent 11725 d0c37d04906b
child 11727 a27150cc8fa5
tuned;
src/FOL/ex/Natural_Numbers.thy
     1.1 --- a/src/FOL/ex/Natural_Numbers.thy	Fri Oct 12 12:06:10 2001 +0200
     1.2 +++ b/src/FOL/ex/Natural_Numbers.thy	Fri Oct 12 12:06:23 2001 +0200
     1.3 @@ -62,8 +62,8 @@
     1.4  
     1.5  lemma "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i + j) = i + f(j)"
     1.6  proof -
     1.7 -  assume a: "!!n. f(Suc(n)) = Suc(f(n))"
     1.8 -  show ?thesis by (induct i) (simp, simp add: a)  (* FIXME tune *)
     1.9 +  assume "!!n. f(Suc(n)) = Suc(f(n))"
    1.10 +  thus ?thesis by (induct i) simp_all
    1.11  qed
    1.12  
    1.13  end