1.1 --- a/src/HOL/Library/Univ_Poly.thy	Mon Sep 13 08:43:48 2010 +0200
     1.2 +++ b/src/HOL/Library/Univ_Poly.thy	Mon Sep 13 11:13:15 2010 +0200
     1.3 @@ -382,7 +382,7 @@
     1.4  lemma (in idom_char_0) poly_entire:
     1.5    "poly (p *** q) = poly [] \<longleftrightarrow> poly p = poly [] \<or> poly q = poly []"
     1.6  using poly_entire_lemma2[of p q]
     1.7 -by (auto simp add: ext_iff poly_mult)
     1.8 +by (auto simp add: fun_eq_iff poly_mult)
     1.9  
    1.10  lemma (in idom_char_0) poly_entire_neg: "(poly (p *** q) \<noteq> poly []) = ((poly p \<noteq> poly []) & (poly q \<noteq> poly []))"
    1.11  by (simp add: poly_entire)
    1.12 @@ -847,14 +847,14 @@
    1.13    assume eq: ?lhs
    1.14    hence "\<And>x. poly ((c#cs) +++ -- (d#ds)) x = 0"
    1.15      by (simp only: poly_minus poly_add algebra_simps) simp
    1.16 -  hence "poly ((c#cs) +++ -- (d#ds)) = poly []" by(simp add: ext_iff)
    1.17 +  hence "poly ((c#cs) +++ -- (d#ds)) = poly []" by(simp add: fun_eq_iff)
    1.18    hence "c = d \<and> list_all (\<lambda>x. x=0) ((cs +++ -- ds))"
    1.19      unfolding poly_zero by (simp add: poly_minus_def algebra_simps)
    1.20    hence "c = d \<and> (\<forall>x. poly (cs +++ -- ds) x = 0)"
    1.21      unfolding poly_zero[symmetric] by simp
    1.22 -  thus ?rhs  by (simp add: poly_minus poly_add algebra_simps ext_iff)
    1.23 +  thus ?rhs  by (simp add: poly_minus poly_add algebra_simps fun_eq_iff)
    1.24  next
    1.25 -  assume ?rhs then show ?lhs by(simp add:ext_iff)
    1.26 +  assume ?rhs then show ?lhs by(simp add:fun_eq_iff)
    1.27  qed
    1.28  
    1.29  lemma (in idom_char_0) pnormalize_unique: "poly p = poly q \<Longrightarrow> pnormalize p = pnormalize q"