src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
changeset 60537 5398aa5a4df9
parent 60533 1e7ccd864b62
child 60580 7e741e22d7fc
     1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sat Jun 20 20:11:22 2015 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sat Jun 20 20:17:29 2015 +0200
     1.3 @@ -1217,7 +1217,7 @@
     1.4        then have "poly (polypoly' (?ts @ xs) p) = poly []"
     1.5          by auto
     1.6        then have "\<forall>c \<in> set (coefficients p). Ipoly (?ts @ xs) (decrpoly c) = 0"
     1.7 -        using poly_zero[where ?'a='a] by (simp add: polypoly'_def list_all_iff)
     1.8 +        using poly_zero[where ?'a='a] by (simp add: polypoly'_def)
     1.9        with coefficients_head[of p, symmetric]
    1.10        have th0: "Ipoly (?ts @ xs) ?hd = 0"
    1.11          by simp