src/HOL/Algebra/Exponent.thy

--- a/src/HOL/Algebra/Exponent.thy	Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Algebra/Exponent.thy	Wed Aug 30 03:19:08 2006 +0200
@@ -327,6 +327,7 @@
 apply (subst times_binomial_minus1_eq, simp, simp)
 apply (subst exponent_mult_add, simp)
 apply (simp (no_asm_simp) add: zero_less_binomial_iff)
+apply arith
 apply (simp del: bad_Sucs add: exponent_mult_add const_p_fac_right)
 done