# HG changeset patch
# User haftmann
# Date 1541836640 0
# Node ID 3d954183b707305984051f0763ac82c110b63d50
# Parent  9bbd5497befdf46b18ac521a636b0464864f239a
replaced some ancient ASCII syntax

diff -r 9bbd5497befd -r 3d954183b707 src/HOL/BNF_Cardinal_Arithmetic.thy
--- 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
 
diff -r 9bbd5497befd -r 3d954183b707 src/HOL/BNF_Cardinal_Order_Relation.thy
--- 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-
diff -r 9bbd5497befd -r 3d954183b707 src/HOL/Lattices_Big.thy
--- 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
diff -r 9bbd5497befd -r 3d954183b707 src/HOL/List.thy
--- 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"
diff -r 9bbd5497befd -r 3d954183b707 src/HOL/Set_Interval.thy
--- 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>
diff -r 9bbd5497befd -r 3d954183b707 src/HOL/Transitive_Closure.thy
--- 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