src/HOL/Library/Univ_Poly.thy

 qed
 
 lemma (in idom_char_0) poly_entire:
   "poly (p *** q) = poly [] \<longleftrightarrow> poly p = poly [] \<or> poly q = poly []"
 using poly_entire_lemma2[of p q]
-by (auto simp add: ext_iff poly_mult)
+by (auto simp add: fun_eq_iff poly_mult)
 
 lemma (in idom_char_0) poly_entire_neg: "(poly (p *** q) \<noteq> poly []) = ((poly p \<noteq> poly []) & (poly q \<noteq> poly []))"
 by (simp add: poly_entire)
 
 lemma fun_eq: " (f = g) = (\<forall>x. f x = g x)"

 lemma (in idom_char_0) poly_Cons_eq: "poly (c#cs) = poly (d#ds) \<longleftrightarrow> c=d \<and> poly cs = poly ds" (is "?lhs \<longleftrightarrow> ?rhs")
 proof
   assume eq: ?lhs
   hence "\<And>x. poly ((c#cs) +++ -- (d#ds)) x = 0"
     by (simp only: poly_minus poly_add algebra_simps) simp
-  hence "poly ((c#cs) +++ -- (d#ds)) = poly []" by(simp add: ext_iff)
+  hence "poly ((c#cs) +++ -- (d#ds)) = poly []" by(simp add: fun_eq_iff)
   hence "c = d \<and> list_all (\<lambda>x. x=0) ((cs +++ -- ds))"
     unfolding poly_zero by (simp add: poly_minus_def algebra_simps)
   hence "c = d \<and> (\<forall>x. poly (cs +++ -- ds) x = 0)"
     unfolding poly_zero[symmetric] by simp
-  thus ?rhs  by (simp add: poly_minus poly_add algebra_simps ext_iff)
+  thus ?rhs  by (simp add: poly_minus poly_add algebra_simps fun_eq_iff)
 next
-  assume ?rhs then show ?lhs by(simp add:ext_iff)
+  assume ?rhs then show ?lhs by(simp add:fun_eq_iff)
 qed
 
 lemma (in idom_char_0) pnormalize_unique: "poly p = poly q \<Longrightarrow> pnormalize p = pnormalize q"
 proof(induct q arbitrary: p)
   case Nil thus ?case by (simp only: poly_zero lemma_degree_zero) simp