changeset 20282 | 49c312eaaa11 |
parent 16733 | 236dfafbeb63 |
child 20318 | 0e0ea63fe768 |
--- a/src/HOL/Algebra/Exponent.thy Wed Aug 02 13:48:21 2006 +0200 +++ b/src/HOL/Algebra/Exponent.thy Wed Aug 02 16:50:41 2006 +0200 @@ -326,7 +326,6 @@ 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