comments for uniformity
authorhaftmann
Sun Mar 18 08:57:45 2012 +0100 (2012-03-18)
changeset 470029435d419109a
parent 47001 a0e370d3d149
child 47003 3094745a41ef
comments for uniformity
src/HOL/Library/Polynomial.thy
     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