src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
changeset 58776 95e58e04e534
parent 58710 7216a10d69ba
child 58834 773b378d9313
     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Fri Oct 24 15:07:49 2014 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Fri Oct 24 15:07:51 2014 +0200
     1.3 @@ -375,7 +375,7 @@
     1.4  
     1.5  lemma polyadd[simp]: "Ipoly bs (polyadd p q) = Ipoly bs p + Ipoly bs q"
     1.6    by (induct p q rule: polyadd.induct)
     1.7 -    (auto simp add: Let_def field_simps distrib_left[symmetric] simp del: distrib_left)
     1.8 +     (auto simp add: Let_def field_simps distrib_left[symmetric] simp del: distrib_left_NO_MATCH)
     1.9  
    1.10  lemma polyadd_norm: "isnpoly p \<Longrightarrow> isnpoly q \<Longrightarrow> isnpoly (polyadd p q)"
    1.11    using polyadd_normh[of "p" "0" "q" "0"] isnpoly_def by simp