src/HOL/Library/Binomial.thy
 changeset 47108 2a1953f0d20d parent 46757 ad878aff9c15 child 48830 72efe3e0a46b
```     1.1 --- a/src/HOL/Library/Binomial.thy	Sat Mar 24 16:27:04 2012 +0100
1.2 +++ b/src/HOL/Library/Binomial.thy	Sun Mar 25 20:15:39 2012 +0200
1.3 @@ -350,7 +350,7 @@
1.4      have eq: "(- (1\<Colon>'a)) ^ n = setprod (\<lambda>i. - 1) {0 .. n - 1}"
1.5        by auto
1.6      from n0 have ?thesis
1.7 -      by (simp add: pochhammer_def gbinomial_def field_simps eq setprod_timesf[symmetric])}
1.8 +      by (simp add: pochhammer_def gbinomial_def field_simps eq setprod_timesf[symmetric] del: minus_one) (* FIXME: del: minus_one *)}
1.9    ultimately show ?thesis by blast
1.10  qed
1.11
1.12 @@ -417,8 +417,8 @@
1.13      from eq[symmetric]
1.14      have ?thesis using kn
1.15        apply (simp add: binomial_fact[OF kn, where ?'a = 'a]
1.16 -        gbinomial_pochhammer field_simps pochhammer_Suc_setprod)
1.17 -      apply (simp add: pochhammer_Suc_setprod fact_altdef_nat h of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def power_Suc)
1.18 +        gbinomial_pochhammer field_simps pochhammer_Suc_setprod del: minus_one)
1.19 +      apply (simp add: pochhammer_Suc_setprod fact_altdef_nat h of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def power_Suc del: minus_one)
1.20        unfolding setprod_Un_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \<Rightarrow> 'a"] eq[unfolded h]
1.21        unfolding mult_assoc[symmetric]
1.22        unfolding setprod_timesf[symmetric]
```