src/HOL/Library/Polynomial.thy
changeset 39302 d7728f65b353
parent 39198 f967a16dfcdd
child 41959 b460124855b8
--- a/src/HOL/Library/Polynomial.thy	Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOL/Library/Polynomial.thy	Mon Sep 13 11:13:15 2010 +0200
@@ -16,7 +16,7 @@
   by auto
 
 lemma expand_poly_eq: "p = q \<longleftrightarrow> (\<forall>n. coeff p n = coeff q n)"
-by (simp add: coeff_inject [symmetric] ext_iff)
+by (simp add: coeff_inject [symmetric] fun_eq_iff)
 
 lemma poly_ext: "(\<And>n. coeff p n = coeff q n) \<Longrightarrow> p = q"
 by (simp add: expand_poly_eq)
@@ -1403,7 +1403,7 @@
   fixes p q :: "'a::{idom,ring_char_0} poly"
   shows "poly p = poly q \<longleftrightarrow> p = q"
   using poly_zero [of "p - q"]
-  by (simp add: ext_iff)
+  by (simp add: fun_eq_iff)
 
 
 subsection {* Composition of polynomials *}