# HG changeset patch
# User wenzelm
# Date 1434824249 -7200
# Node ID 5398aa5a4df9b58fb8349e13fefbf3ca516dbd6d
# Parent  00db0d934a7dc25b7d5907bd1a5740b2d8ae30d4
eliminated list_all;

diff -r 00db0d934a7d -r 5398aa5a4df9 src/HOL/Decision_Procs/Polynomial_List.thy
--- a/src/HOL/Decision_Procs/Polynomial_List.thy	Sat Jun 20 20:11:22 2015 +0200
+++ b/src/HOL/Decision_Procs/Polynomial_List.thy	Sat Jun 20 20:17:29 2015 +0200
@@ -498,7 +498,7 @@
     by simp
 qed
 
-lemma (in idom_char_0) poly_zero: "poly p = poly [] \<longleftrightarrow> list_all (\<lambda>c. c = 0) p"
+lemma (in idom_char_0) poly_zero: "poly p = poly [] \<longleftrightarrow> (\<forall>c \<in> set p. c = 0)"
   apply (induct p)
   apply simp
   apply (rule iffI)
@@ -506,7 +506,7 @@
   apply auto
   done
 
-lemma (in idom_char_0) poly_0: "list_all (\<lambda>c. c = 0) p \<Longrightarrow> poly p x = 0"
+lemma (in idom_char_0) poly_0: "\<forall>c \<in> set p. c = 0 \<Longrightarrow> poly p x = 0"
   unfolding poly_zero[symmetric] by simp
 
 
@@ -873,7 +873,7 @@
 
 text \<open>The degree of a polynomial.\<close>
 
-lemma (in semiring_0) lemma_degree_zero: "list_all (\<lambda>c. c = 0) p \<longleftrightarrow> pnormalize p = []"
+lemma (in semiring_0) lemma_degree_zero: "(\<forall>c \<in> set p. c = 0) \<longleftrightarrow> pnormalize p = []"
   by (induct p) auto
 
 lemma (in idom_char_0) degree_zero:
@@ -916,7 +916,7 @@
       by (simp only: poly_minus poly_add algebra_simps) (simp add: algebra_simps)
     then have "poly ((c # cs) +++ -- (d # ds)) = poly []"
       by (simp add: fun_eq_iff)
-    then have "c = d" and "list_all (\<lambda>x. x = 0) ((cs +++ -- ds))"
+    then have "c = d" and "\<forall>x \<in> set (cs +++ -- ds). x = 0"
       unfolding poly_zero by (simp_all add: poly_minus_def algebra_simps)
     from this(2) have "poly (cs +++ -- ds) x = 0" for x
       unfolding poly_zero[symmetric] by simp
diff -r 00db0d934a7d -r 5398aa5a4df9 src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
--- 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