src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
changeset 49962 a8cc904a6820
parent 46991 196f2d9406c4
child 50282 fe4d4bb9f4c2
     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Fri Oct 19 10:46:42 2012 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Fri Oct 19 15:12:52 2012 +0200
     1.3 @@ -304,7 +304,7 @@
     1.4  qed auto
     1.5  
     1.6  lemma polyadd[simp]: "Ipoly bs (polyadd p q) = Ipoly bs p + Ipoly bs q"
     1.7 -by (induct p q rule: polyadd.induct, auto simp add: Let_def field_simps right_distrib[symmetric] simp del: right_distrib)
     1.8 +by (induct p q rule: polyadd.induct, auto simp add: Let_def field_simps distrib_left[symmetric] simp del: distrib_left)
     1.9  
    1.10  lemma polyadd_norm: "\<lbrakk> isnpoly p ; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polyadd p q)"
    1.11    using polyadd_normh[of "p" "0" "q" "0"] isnpoly_def by simp