--- a/src/HOL/Algebra/poly/UnivPoly2.thy Wed Aug 02 13:48:21 2006 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy Wed Aug 02 16:50:41 2006 +0200
@@ -187,6 +187,8 @@
by (simp add: coeff_def up_add_def Abs_UP_inverse Rep_UP)
qed
+ML {* fast_arith_split_limit := 0; *} (* FIXME: rewrite proof *)
+
lemma coeff_mult [simp]:
"coeff (p * q) n = (setsum (%i. coeff p i * coeff q (n-i)) {..n}::'a::ring)"
proof -
@@ -226,6 +228,8 @@
by (simp add: coeff_def up_mult_def Abs_UP_inverse Rep_UP)
qed
+ML {* fast_arith_split_limit := 9; *} (* FIXME *)
+
lemma coeff_uminus [simp]: "coeff (-p) n = (-coeff p n::'a::ring)"
by (unfold up_uminus_def) (simp add: ring_simps)