src/HOL/BNF_Cardinal_Arithmetic.thy

--- a/src/HOL/BNF_Cardinal_Arithmetic.thy	Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/BNF_Cardinal_Arithmetic.thy	Thu Feb 15 12:11:00 2018 +0100
@@ -689,7 +689,7 @@
 
 lemma cardSuc_UNION_Cinfinite:
   assumes "Cinfinite r" "relChain (cardSuc r) As" "B \<le> (UN i : Field (cardSuc r). As i)" "|B| <=o r"
-  shows "EX i : Field (cardSuc r). B \<le> As i"
+  shows "\<exists>i \<in> Field (cardSuc r). B \<le> As i"
 using cardSuc_UNION assms unfolding cinfinite_def by blast
 
 end