src/HOL/Library/Binomial.thy

--- a/src/HOL/Library/Binomial.thy	Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOL/Library/Binomial.thy	Mon Sep 13 11:13:15 2010 +0200
@@ -236,7 +236,7 @@
     have th1: "(\<Prod>n\<in>{1\<Colon>nat..n}. a + of_nat n) =
       (\<Prod>n\<in>{0\<Colon>nat..n - 1}. a + 1 + of_nat n)"
       apply (rule setprod_reindex_cong [where f = Suc])
-      using n0 by (auto simp add: ext_iff field_simps)
+      using n0 by (auto simp add: fun_eq_iff field_simps)
     have ?thesis apply (simp add: pochhammer_def)
     unfolding setprod_insert[OF th0, unfolded eq]
     using th1 by (simp add: field_simps)}
@@ -248,7 +248,7 @@
   
   apply (cases n, simp_all add: of_nat_setprod pochhammer_Suc_setprod)
   apply (rule setprod_reindex_cong[where f=Suc])
-  by (auto simp add: ext_iff)
+  by (auto simp add: fun_eq_iff)
 
 lemma pochhammer_of_nat_eq_0_lemma: assumes kn: "k > n"
   shows "pochhammer (- (of_nat n :: 'a:: idom)) k = 0"
@@ -315,7 +315,7 @@
       apply (rule strong_setprod_reindex_cong[where f = "%i. h - i"])
       apply (auto simp add: inj_on_def image_def h )
       apply (rule_tac x="h - x" in bexI)
-      by (auto simp add: ext_iff h of_nat_diff)}
+      by (auto simp add: fun_eq_iff h of_nat_diff)}
   ultimately show ?thesis by (cases k, auto)
 qed
 
@@ -410,11 +410,11 @@
     have eq': "(\<Prod>i\<in>{0..h}. of_nat n + - (of_nat i :: 'a)) = (\<Prod>i\<in>{n - h..n}. of_nat i)"
       apply (rule strong_setprod_reindex_cong[where f="op - n"])
       using h kn 
-      apply (simp_all add: inj_on_def image_iff Bex_def set_ext_iff)
+      apply (simp_all add: inj_on_def image_iff Bex_def set_eq_iff)
       apply clarsimp
       apply (presburger)
       apply presburger
-      by (simp add: ext_iff field_simps of_nat_add[symmetric] del: of_nat_add)
+      by (simp add: fun_eq_iff field_simps of_nat_add[symmetric] del: of_nat_add)
     have th0: "finite {1..n - Suc h}" "finite {n - h .. n}" 
 "{1..n - Suc h} \<inter> {n - h .. n} = {}" and eq3: "{1..n - Suc h} \<union> {n - h .. n} = {1..n}" using h kn by auto
     from eq[symmetric]