src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
changeset 45129 1fce03e3e8ad
parent 41842 d8f76db6a207
child 46991 196f2d9406c4
     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Wed Oct 12 16:21:07 2011 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Wed Oct 12 20:16:48 2011 +0200
     1.3 @@ -693,7 +693,7 @@
     1.4    by (simp add: funpow_shift1)
     1.5  
     1.6  lemma poly_cmul[simp]: "Ipoly bs (poly_cmul c p) = Ipoly bs (Mul (C c) p)"
     1.7 -by (induct p  arbitrary: n0 rule: poly_cmul.induct, auto simp add: field_simps)
     1.8 +  by (induct p rule: poly_cmul.induct) (auto simp add: field_simps)
     1.9  
    1.10  lemma behead:
    1.11    assumes np: "isnpolyh p n"