1.1 --- a/src/HOL/Library/Polynomial.thy Sat Mar 17 23:55:03 2012 +0100
1.2 +++ b/src/HOL/Library/Polynomial.thy Sun Mar 18 08:57:45 2012 +0100
1.3 @@ -17,9 +17,11 @@
1.4 morphisms coeff Abs_poly
1.5 unfolding Poly_def by auto
1.6
1.7 +(* FIXME should be named poly_eq_iff *)
1.8 lemma expand_poly_eq: "p = q \<longleftrightarrow> (\<forall>n. coeff p n = coeff q n)"
1.9 by (simp add: coeff_inject [symmetric] fun_eq_iff)
1.10
1.11 +(* FIXME should be named poly_eqI *)
1.12 lemma poly_ext: "(\<And>n. coeff p n = coeff q n) \<Longrightarrow> p = q"
1.13 by (simp add: expand_poly_eq)
1.14