--- a/src/HOL/BNF_Cardinal_Arithmetic.thy Sat Nov 10 07:57:19 2018 +0000
+++ b/src/HOL/BNF_Cardinal_Arithmetic.thy Sat Nov 10 07:57:20 2018 +0000
@@ -688,7 +688,7 @@
by (simp add: cinfinite_def cardSuc_Card_order cardSuc_finite)
lemma cardSuc_UNION_Cinfinite:
- assumes "Cinfinite r" "relChain (cardSuc r) As" "B \<le> (UN i : Field (cardSuc r). As i)" "|B| <=o r"
+ assumes "Cinfinite r" "relChain (cardSuc r) As" "B \<le> (\<Union>i \<in> Field (cardSuc r). As i)" "|B| <=o r"
shows "\<exists>i \<in> Field (cardSuc r). B \<le> As i"
using cardSuc_UNION assms unfolding cinfinite_def by blast
--- a/src/HOL/BNF_Cardinal_Order_Relation.thy Sat Nov 10 07:57:19 2018 +0000
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy Sat Nov 10 07:57:20 2018 +0000
@@ -1519,7 +1519,7 @@
lemma regularCard_UNION:
assumes r: "Card_order r" "regularCard r"
and As: "relChain r As"
-and Bsub: "B \<le> (UN i : Field r. As i)"
+and Bsub: "B \<le> (\<Union>i \<in> Field r. As i)"
and cardB: "|B| <o r"
shows "\<exists>i \<in> Field r. B \<le> As i"
proof-
@@ -1568,7 +1568,7 @@
using r' by (simp add: card_of_Field_ordIso[of ?r'])
finally have "|K| \<le>o ?r'" .
moreover
- {let ?L = "UN j : K. underS ?r' j"
+ {let ?L = "\<Union> j \<in> K. underS ?r' j"
let ?J = "Field r"
have rJ: "r =o |?J|"
using r_card card_of_Field_ordIso ordIso_symmetric by blast
@@ -1606,7 +1606,7 @@
lemma cardSuc_UNION:
assumes r: "Card_order r" and "\<not>finite (Field r)"
and As: "relChain (cardSuc r) As"
-and Bsub: "B \<le> (UN i : Field (cardSuc r). As i)"
+and Bsub: "B \<le> (\<Union> i \<in> Field (cardSuc r). As i)"
and cardB: "|B| <=o r"
shows "\<exists>i \<in> Field (cardSuc r). B \<le> As i"
proof-
--- a/src/HOL/Lattices_Big.thy Sat Nov 10 07:57:19 2018 +0000
+++ b/src/HOL/Lattices_Big.thy Sat Nov 10 07:57:20 2018 +0000
@@ -370,7 +370,7 @@
by (rule finite_surj [where f = "sup x", OF B(1)], auto)
have finAB: "finite {sup a b |a b. a \<in> A \<and> b \<in> B}"
proof -
- have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})"
+ have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (\<Union>a\<in>A. \<Union>b\<in>B. {sup a b})"
by blast
thus ?thesis by(simp add: insert(1) B(1))
qed
@@ -407,7 +407,7 @@
by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto)
have finAB: "finite {inf a b |a b. a \<in> A \<and> b \<in> B}"
proof -
- have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {inf a b})"
+ have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (\<Union>a\<in>A. \<Union>b\<in>B. {inf a b})"
by blast
thus ?thesis by(simp add: insert(1) B(1))
qed
--- a/src/HOL/List.thy Sat Nov 10 07:57:19 2018 +0000
+++ b/src/HOL/List.thy Sat Nov 10 07:57:20 2018 +0000
@@ -1633,7 +1633,7 @@
lemma Nil_eq_concat_conv [simp]: "([] = concat xss) = (\<forall>xs \<in> set xss. xs = [])"
by (induct xss) auto
-lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)"
+lemma set_concat [simp]: "set (concat xs) = (\<Union>x\<in>set xs. set x)"
by (induct xs) auto
lemma concat_map_singleton[simp]: "concat(map (%x. [f x]) xs) = map f xs"
--- a/src/HOL/Set_Interval.thy Sat Nov 10 07:57:19 2018 +0000
+++ b/src/HOL/Set_Interval.thy Sat Nov 10 07:57:20 2018 +0000
@@ -696,7 +696,7 @@
lemma atMost_Suc_eq_insert_0: "{.. Suc n} = insert 0 (Suc ` {.. n})"
unfolding lessThan_Suc_atMost[symmetric] lessThan_Suc_eq_insert_0[of "Suc n"] ..
-lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV"
+lemma UN_lessThan_UNIV: "(\<Union>m::nat. lessThan m) = UNIV"
by blast
subsubsection \<open>The Constant @{term greaterThan}\<close>
@@ -709,7 +709,7 @@
unfolding greaterThan_def
by (auto elim: linorder_neqE)
-lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}"
+lemma INT_greaterThan_UNIV: "(\<Inter>m::nat. greaterThan m) = {}"
by blast
subsubsection \<open>The Constant @{term atLeast}\<close>
@@ -723,7 +723,7 @@
lemma atLeast_Suc_greaterThan: "atLeast (Suc k) = greaterThan k"
by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le)
-lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV"
+lemma UN_atLeast_UNIV: "(\<Union>m::nat. atLeast m) = UNIV"
by blast
subsubsection \<open>The Constant @{term atMost}\<close>
@@ -734,7 +734,7 @@
lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)"
unfolding atMost_def by (auto simp add: less_Suc_eq order_le_less)
-lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV"
+lemma UN_atMost_UNIV: "(\<Union>m::nat. atMost m) = UNIV"
by blast
subsubsection \<open>The Constant @{term atLeastLessThan}\<close>
--- a/src/HOL/Transitive_Closure.thy Sat Nov 10 07:57:19 2018 +0000
+++ b/src/HOL/Transitive_Closure.thy Sat Nov 10 07:57:20 2018 +0000
@@ -1064,7 +1064,7 @@
lemma relpow_finite_bounded:
fixes R :: "('a \<times> 'a) set"
assumes "finite R"
- shows "R^^k \<subseteq> (UN n:{n. n \<le> card R}. R^^n)"
+ shows "R^^k \<subseteq> (\<Union>n\<in>{n. n \<le> card R}. R^^n)"
apply (cases k, force)
apply (use relpow_finite_bounded1[OF assms, of k] in auto)
done