src/HOL/Library/Binomial.thy
 changeset 39302 d7728f65b353 parent 39198 f967a16dfcdd child 46507 1b24c24017dd
```     1.1 --- a/src/HOL/Library/Binomial.thy	Mon Sep 13 08:43:48 2010 +0200
1.2 +++ b/src/HOL/Library/Binomial.thy	Mon Sep 13 11:13:15 2010 +0200
1.3 @@ -236,7 +236,7 @@
1.4      have th1: "(\<Prod>n\<in>{1\<Colon>nat..n}. a + of_nat n) =
1.5        (\<Prod>n\<in>{0\<Colon>nat..n - 1}. a + 1 + of_nat n)"
1.6        apply (rule setprod_reindex_cong [where f = Suc])
1.7 -      using n0 by (auto simp add: ext_iff field_simps)
1.8 +      using n0 by (auto simp add: fun_eq_iff field_simps)
1.9      have ?thesis apply (simp add: pochhammer_def)
1.10      unfolding setprod_insert[OF th0, unfolded eq]
1.11      using th1 by (simp add: field_simps)}
1.12 @@ -248,7 +248,7 @@
1.13
1.14    apply (cases n, simp_all add: of_nat_setprod pochhammer_Suc_setprod)
1.15    apply (rule setprod_reindex_cong[where f=Suc])
1.16 -  by (auto simp add: ext_iff)
1.17 +  by (auto simp add: fun_eq_iff)
1.18
1.19  lemma pochhammer_of_nat_eq_0_lemma: assumes kn: "k > n"
1.20    shows "pochhammer (- (of_nat n :: 'a:: idom)) k = 0"
1.21 @@ -315,7 +315,7 @@
1.22        apply (rule strong_setprod_reindex_cong[where f = "%i. h - i"])
1.23        apply (auto simp add: inj_on_def image_def h )
1.24        apply (rule_tac x="h - x" in bexI)
1.25 -      by (auto simp add: ext_iff h of_nat_diff)}
1.26 +      by (auto simp add: fun_eq_iff h of_nat_diff)}
1.27    ultimately show ?thesis by (cases k, auto)
1.28  qed
1.29
1.30 @@ -410,11 +410,11 @@
1.31      have eq': "(\<Prod>i\<in>{0..h}. of_nat n + - (of_nat i :: 'a)) = (\<Prod>i\<in>{n - h..n}. of_nat i)"
1.32        apply (rule strong_setprod_reindex_cong[where f="op - n"])
1.33        using h kn
1.34 -      apply (simp_all add: inj_on_def image_iff Bex_def set_ext_iff)
1.35 +      apply (simp_all add: inj_on_def image_iff Bex_def set_eq_iff)
1.36        apply clarsimp
1.37        apply (presburger)
1.38        apply presburger