--- a/src/HOL/IMP/Fold.thy Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/IMP/Fold.thy Thu Feb 15 12:11:00 2018 +0100
@@ -11,7 +11,7 @@
"afold (Plus e1 e2) t = (case (afold e1 t, afold e2 t) of
(N n1, N n2) \<Rightarrow> N(n1+n2) | (e1',e2') \<Rightarrow> Plus e1' e2')"
-definition "approx t s \<longleftrightarrow> (ALL x k. t x = Some k \<longrightarrow> s x = k)"
+definition "approx t s \<longleftrightarrow> (\<forall>x k. t x = Some k \<longrightarrow> s x = k)"
theorem aval_afold[simp]:
assumes "approx t s"