Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
changeset 60537 5398aa5a4df9
parent 60533 1e7ccd864b62
child 60580 7e741e22d7fc 
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sat Jun 20 20:11:22 2015 +0200
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sat Jun 20 20:17:29 2015 +0200
@@ -1217,7 +1217,7 @@
       then have "poly (polypoly' (?ts @ xs) p) = poly []"
         by auto
       then have "\<forall>c \<in> set (coefficients p). Ipoly (?ts @ xs) (decrpoly c) = 0"
-        using poly_zero[where ?'a='a] by (simp add: polypoly'_def list_all_iff)
+        using poly_zero[where ?'a='a] by (simp add: polypoly'_def)
       with coefficients_head[of p, symmetric]
       have th0: "Ipoly (?ts @ xs) ?hd = 0"
         by simp
isabelle