--- a/src/HOL/Library/IArray.thy Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/Library/IArray.thy Thu Feb 15 12:11:00 2018 +0100
@@ -31,10 +31,10 @@
[simp]: "length as = List.length (IArray.list_of as)"
qualified fun all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
-"all p (IArray as) = (ALL a : set as. p a)"
+"all p (IArray as) = (\<forall>a \<in> set as. p a)"
qualified fun exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
-"exists p (IArray as) = (EX a : set as. p a)"
+"exists p (IArray as) = (\<exists>a \<in> set as. p a)"
lemma list_of_code [code]:
"IArray.list_of as = map (\<lambda>n. as !! n) [0 ..< IArray.length as]"