1.1 --- a/src/HOL/Binomial.thy	Wed Jul 26 13:31:07 2006 +0200
     1.2 +++ b/src/HOL/Binomial.thy	Wed Jul 26 19:23:04 2006 +0200
     1.3 @@ -33,9 +33,8 @@
     1.4  by simp
     1.5  
     1.6  lemma binomial_eq_0 [rule_format]: "\<forall>k. n < k --> (n choose k) = 0"
     1.7 -apply (induct "n", auto)
     1.8 -apply (erule allE)
     1.9 -apply (erule mp, arith)
    1.10 +apply (induct "n")
    1.11 +apply auto
    1.12  done
    1.13  
    1.14  declare binomial_0 [simp del] binomial_Suc [simp del]