src/HOL/Algebra/poly/UnivPoly2.thy

 (*
   Title:     Univariate Polynomials
-  Id:        $Id$
   Author:    Clemens Ballarin, started 9 December 1996
   Copyright: Clemens Ballarin
 *)
 
 header {* Univariate Polynomials *}

   fix k
   have "coeff (p * monom a 0) k = coeff (a *s p) k"
   proof (cases k)
     case 0 then show ?thesis by simp ring
   next
-    case Suc then show ?thesis by (simp add: algebra_simps) ring
+    case Suc then show ?thesis by simp (ring, simp)
   qed
   then show "coeff (monom a 0 * p) k = coeff (a *s p) k" by ring
 qed
 
 ML {* Addsimprocs [ring_simproc] *}