src/HOL/Library/Polynomial.thy
changeset 39302 d7728f65b353
parent 39198 f967a16dfcdd
child 41959 b460124855b8
     1.1 --- a/src/HOL/Library/Polynomial.thy	Mon Sep 13 08:43:48 2010 +0200
     1.2 +++ b/src/HOL/Library/Polynomial.thy	Mon Sep 13 11:13:15 2010 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4    by auto
     1.5  
     1.6  lemma expand_poly_eq: "p = q \<longleftrightarrow> (\<forall>n. coeff p n = coeff q n)"
     1.7 -by (simp add: coeff_inject [symmetric] ext_iff)
     1.8 +by (simp add: coeff_inject [symmetric] fun_eq_iff)
     1.9  
    1.10  lemma poly_ext: "(\<And>n. coeff p n = coeff q n) \<Longrightarrow> p = q"
    1.11  by (simp add: expand_poly_eq)
    1.12 @@ -1403,7 +1403,7 @@
    1.13    fixes p q :: "'a::{idom,ring_char_0} poly"
    1.14    shows "poly p = poly q \<longleftrightarrow> p = q"
    1.15    using poly_zero [of "p - q"]
    1.16 -  by (simp add: ext_iff)
    1.17 +  by (simp add: fun_eq_iff)
    1.18  
    1.19  
    1.20  subsection {* Composition of polynomials *}