# HG changeset patch
# User haftmann
# Date 1332057465 -3600
# Node ID 9435d419109a1e6d5d4566080bd73d923ec86e28
# Parent  a0e370d3d149dacd83da2c6022a3b9f8e085d48f
comments for uniformity

diff -r a0e370d3d149 -r 9435d419109a src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Sat Mar 17 23:55:03 2012 +0100
+++ b/src/HOL/Library/Polynomial.thy	Sun Mar 18 08:57:45 2012 +0100
@@ -17,9 +17,11 @@
   morphisms coeff Abs_poly
   unfolding Poly_def by auto
 
+(* FIXME should be named poly_eq_iff *)
 lemma expand_poly_eq: "p = q \<longleftrightarrow> (\<forall>n. coeff p n = coeff q n)"
   by (simp add: coeff_inject [symmetric] fun_eq_iff)
 
+(* FIXME should be named poly_eqI *)
 lemma poly_ext: "(\<And>n. coeff p n = coeff q n) \<Longrightarrow> p = q"
   by (simp add: expand_poly_eq)