# HG changeset patch
# User haftmann
# Date 1541836639 0
# Node ID 9bbd5497befdf46b18ac521a636b0464864f239a
# Parent  ff7e6751a1a7a75fd54194eed02fa24cc9c4729a
clarified status of legacy input abbreviations

diff -r ff7e6751a1a7 -r 9bbd5497befd src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Sat Nov 10 07:57:18 2018 +0000
+++ b/src/HOL/Complete_Lattices.thy	Sat Nov 10 07:57:19 2018 +0000
@@ -16,21 +16,9 @@
 
 class Inf =
   fixes Inf :: "'a set \<Rightarrow> 'a"  ("\<Sqinter> _" [900] 900)
-begin
-
-abbreviation (input) INFIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" \<comment> \<open>legacy\<close>
-  where "INFIMUM A f \<equiv> \<Sqinter>(f ` A)"
-
-end
 
 class Sup =
   fixes Sup :: "'a set \<Rightarrow> 'a"  ("\<Squnion> _" [900] 900)
-begin
-
-abbreviation (input) SUPREMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" \<comment> \<open>legacy\<close>
-  where "SUPREMUM A f \<equiv> \<Squnion>(f ` A)"
-
-end
 
 syntax (ASCII)
   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3INF _./ _)" [0, 10] 10)
@@ -858,9 +846,6 @@
 
 subsubsection \<open>Intersections of families\<close>
 
-abbreviation (input) INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" \<comment> \<open>legacy\<close>
-  where "INTER \<equiv> INFIMUM"
-
 syntax (ASCII)
   "_INTER1"     :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set"           ("(3INT _./ _)" [0, 10] 10)
   "_INTER"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set"  ("(3INT _:_./ _)" [0, 0, 10] 10)
@@ -915,7 +900,7 @@
 lemma INT_subset_iff: "B \<subseteq> (\<Inter>i\<in>I. A i) \<longleftrightarrow> (\<forall>i\<in>I. B \<subseteq> A i)"
   by (fact le_INF_iff)
 
-lemma INT_insert [simp]: "(\<Inter>x \<in> insert a A. B x) = B a \<inter> INTER A B"
+lemma INT_insert [simp]: "(\<Inter>x \<in> insert a A. B x) = B a \<inter> \<Inter> (B ` A)"
   by (fact INF_insert)
 
 lemma INT_Un: "(\<Inter>i \<in> A \<union> B. M i) = (\<Inter>i \<in> A. M i) \<inter> (\<Inter>i\<in>B. M i)"
@@ -1018,9 +1003,6 @@
 
 subsubsection \<open>Unions of families\<close>
 
-abbreviation (input) UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" \<comment> \<open>legacy\<close>
-  where "UNION \<equiv> SUPREMUM"
-
 syntax (ASCII)
   "_UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" [0, 10] 10)
   "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3UN _:_./ _)" [0, 0, 10] 10)
@@ -1050,10 +1032,10 @@
 lemma UNION_eq: "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
   by (auto intro!: SUP_eqI)
 
-lemma bind_UNION [code]: "Set.bind A f = UNION A f"
+lemma bind_UNION [code]: "Set.bind A f = \<Union>(f ` A)"
   by (simp add: bind_def UNION_eq)
 
-lemma member_bind [simp]: "x \<in> Set.bind P f \<longleftrightarrow> x \<in> UNION P f "
+lemma member_bind [simp]: "x \<in> Set.bind A f \<longleftrightarrow> x \<in> \<Union>(f ` A)"
   by (simp add: bind_UNION)
 
 lemma Union_SetCompr_eq: "\<Union>{f x| x. P x} = {a. \<exists>x. P x \<and> a \<in> f x}"
@@ -1091,7 +1073,7 @@
 lemma UN_absorb: "k \<in> I \<Longrightarrow> A k \<union> (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. A i)"
   by (fact SUP_absorb)
 
-lemma UN_insert [simp]: "(\<Union>x\<in>insert a A. B x) = B a \<union> UNION A B"
+lemma UN_insert [simp]: "(\<Union>x\<in>insert a A. B x) = B a \<union> \<Union>(B ` A)"
   by (fact SUP_insert)
 
 lemma UN_Un [simp]: "(\<Union>i \<in> A \<union> B. M i) = (\<Union>i\<in>A. M i) \<union> (\<Union>i\<in>B. M i)"
@@ -1120,10 +1102,10 @@
 lemma Collect_ex_eq: "{x. \<exists>y. P x y} = (\<Union>y. {x. P x y})"
   by blast
 
-lemma ball_UN: "(\<forall>z \<in> UNION A B. P z) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>z \<in> B x. P z)"
+lemma ball_UN: "(\<forall>z \<in> \<Union>(B ` A). P z) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>z \<in> B x. P z)"
   by blast
 
-lemma bex_UN: "(\<exists>z \<in> UNION A B. P z) \<longleftrightarrow> (\<exists>x\<in>A. \<exists>z\<in>B x. P z)"
+lemma bex_UN: "(\<exists>z \<in> \<Union>(B ` A). P z) \<longleftrightarrow> (\<exists>x\<in>A. \<exists>z\<in>B x. P z)"
   by blast
 
 lemma Un_eq_UN: "A \<union> B = (\<Union>b. if b then A else B)"
@@ -1150,7 +1132,7 @@
   \<comment> \<open>NOT suitable for rewriting\<close>
   by blast
 
-lemma image_UN: "f ` UNION A B = (\<Union>x\<in>A. f ` B x)"
+lemma image_UN: "f ` \<Union>(B ` A) = (\<Union>x\<in>A. f ` B x)"
   by blast
 
 lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
@@ -1251,14 +1233,14 @@
 proof safe
   have "\<And>i. i \<in> I \<Longrightarrow> inj_on f (A i)"
     using bij bij_betw_def[of f] by auto
-  then show "inj_on f (UNION I A)"
+  then show "inj_on f (\<Union>(A ` I))"
     using chain inj_on_UNION_chain[of I A f] by auto
 next
   fix i x
   assume *: "i \<in> I" "x \<in> A i"
   with bij have "f x \<in> A' i"
     by (auto simp: bij_betw_def)
-  with * show "f x \<in> UNION I A'" by blast
+  with * show "f x \<in> \<Union>(A' ` I)" by blast
 next
   fix i x'
   assume *: "i \<in> I" "x' \<in> A' i"
@@ -1266,18 +1248,18 @@
     unfolding bij_betw_def by blast
   with * have "\<exists>j \<in> I. \<exists>x \<in> A j. x' = f x"
     by blast
-  then show "x' \<in> f ` UNION I A"
+  then show "x' \<in> f ` \<Union>(A ` I)"
     by blast
 qed
 
 (*injectivity's required.  Left-to-right inclusion holds even if A is empty*)
-lemma image_INT: "inj_on f C \<Longrightarrow> \<forall>x\<in>A. B x \<subseteq> C \<Longrightarrow> j \<in> A \<Longrightarrow> f ` (INTER A B) = (INT x:A. f ` B x)"
+lemma image_INT: "inj_on f C \<Longrightarrow> \<forall>x\<in>A. B x \<subseteq> C \<Longrightarrow> j \<in> A \<Longrightarrow> f ` (\<Inter>(B ` A)) = (\<Inter>x\<in>A. f ` B x)"
   by (auto simp add: inj_on_def) blast
 
-lemma bij_image_INT: "bij f \<Longrightarrow> f ` (INTER A B) = (INT x:A. f ` B x)"
+lemma bij_image_INT: "bij f \<Longrightarrow> f ` (\<Inter>(B ` A)) = (\<Inter>x\<in>A. f ` B x)"
   by (auto simp: bij_def inj_def surj_def) blast
 
-lemma UNION_fun_upd: "UNION J (A(i := B)) = UNION (J - {i}) A \<union> (if i \<in> J then B else {})"
+lemma UNION_fun_upd: "\<Union>(A(i := B) ` J) = \<Union>(A ` (J - {i})) \<union> (if i \<in> J then B else {})"
   by (auto simp add: set_eq_iff)
 
 lemma bij_betw_Pow:
@@ -1321,7 +1303,7 @@
   "\<And>A B C. (\<Union>x\<in>C. A x - B) = ((\<Union>x\<in>C. A x) - B)"
   "\<And>A B C. (\<Union>x\<in>C. A - B x) = (A - (\<Inter>x\<in>C. B x))"
   "\<And>A B. (\<Union>x\<in>\<Union>A. B x) = (\<Union>y\<in>A. \<Union>x\<in>y. B x)"
-  "\<And>A B C. (\<Union>z\<in>UNION A B. C z) = (\<Union>x\<in>A. \<Union>z\<in>B x. C z)"
+  "\<And>A B C. (\<Union>z\<in>(\<Union>(B ` A)). C z) = (\<Union>x\<in>A. \<Union>z\<in>B x. C z)"
   "\<And>A B f. (\<Union>x\<in>f`A. B x) = (\<Union>a\<in>A. B (f a))"
   by auto
 
@@ -1334,15 +1316,15 @@
   "\<And>A B C. (\<Inter>x\<in>C. A x \<union> B) = ((\<Inter>x\<in>C. A x) \<union> B)"
   "\<And>A B C. (\<Inter>x\<in>C. A \<union> B x) = (A \<union> (\<Inter>x\<in>C. B x))"
   "\<And>A B. (\<Inter>x\<in>\<Union>A. B x) = (\<Inter>y\<in>A. \<Inter>x\<in>y. B x)"
-  "\<And>A B C. (\<Inter>z\<in>UNION A B. C z) = (\<Inter>x\<in>A. \<Inter>z\<in>B x. C z)"
+  "\<And>A B C. (\<Inter>z\<in>(\<Union>(B ` A)). C z) = (\<Inter>x\<in>A. \<Inter>z\<in>B x. C z)"
   "\<And>A B f. (\<Inter>x\<in>f`A. B x) = (\<Inter>a\<in>A. B (f a))"
   by auto
 
 lemma UN_ball_bex_simps [simp]:
   "\<And>A P. (\<forall>x\<in>\<Union>A. P x) \<longleftrightarrow> (\<forall>y\<in>A. \<forall>x\<in>y. P x)"
-  "\<And>A B P. (\<forall>x\<in>UNION A B. P x) = (\<forall>a\<in>A. \<forall>x\<in> B a. P x)"
+  "\<And>A B P. (\<forall>x\<in>(\<Union>(B ` A)). P x) = (\<forall>a\<in>A. \<forall>x\<in> B a. P x)"
   "\<And>A P. (\<exists>x\<in>\<Union>A. P x) \<longleftrightarrow> (\<exists>y\<in>A. \<exists>x\<in>y. P x)"
-  "\<And>A B P. (\<exists>x\<in>UNION A B. P x) \<longleftrightarrow> (\<exists>a\<in>A. \<exists>x\<in>B a. P x)"
+  "\<And>A B P. (\<exists>x\<in>(\<Union>(B ` A)). P x) \<longleftrightarrow> (\<exists>a\<in>A. \<exists>x\<in>B a. P x)"
   by auto
 
 
@@ -1357,7 +1339,7 @@
   "\<And>A B C. ((\<Union>x\<in>C. A x) - B) = (\<Union>x\<in>C. A x - B)"
   "\<And>A B C. (A - (\<Inter>x\<in>C. B x)) = (\<Union>x\<in>C. A - B x)"
   "\<And>A B. (\<Union>y\<in>A. \<Union>x\<in>y. B x) = (\<Union>x\<in>\<Union>A. B x)"
-  "\<And>A B C. (\<Union>x\<in>A. \<Union>z\<in>B x. C z) = (\<Union>z\<in>UNION A B. C z)"
+  "\<And>A B C. (\<Union>x\<in>A. \<Union>z\<in>B x. C z) = (\<Union>z\<in>(\<Union>(B ` A)). C z)"
   "\<And>A B f. (\<Union>a\<in>A. B (f a)) = (\<Union>x\<in>f`A. B x)"
   by auto
 
@@ -1370,7 +1352,7 @@
   "\<And>A B C. ((\<Inter>x\<in>C. A x) \<union> B) = (\<Inter>x\<in>C. A x \<union> B)"
   "\<And>A B C. A \<union> (\<Inter>x\<in>C. B x) = (\<Inter>x\<in>C. A \<union> B x)"
   "\<And>A B. (\<Inter>y\<in>A. \<Inter>x\<in>y. B x) = (\<Inter>x\<in>\<Union>A. B x)"
-  "\<And>A B C. (\<Inter>x\<in>A. \<Inter>z\<in>B x. C z) = (\<Inter>z\<in>UNION A B. C z)"
+  "\<And>A B C. (\<Inter>x\<in>A. \<Inter>z\<in>B x. C z) = (\<Inter>z\<in>(\<Union>(B ` A)). C z)"
   "\<And>A B f. (\<Inter>a\<in>A. B (f a)) = (\<Inter>x\<in>f`A. B x)"
   by auto
 
diff -r ff7e6751a1a7 -r 9bbd5497befd src/HOL/Conditionally_Complete_Lattices.thy
--- a/src/HOL/Conditionally_Complete_Lattices.thy	Sat Nov 10 07:57:18 2018 +0000
+++ b/src/HOL/Conditionally_Complete_Lattices.thy	Sat Nov 10 07:57:19 2018 +0000
@@ -286,22 +286,22 @@
 lemma cInf_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Inf {y..x} = y"
   by (auto intro!: cInf_eq_minimum)
 
-lemma cINF_lower: "bdd_below (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> INFIMUM A f \<le> f x"
+lemma cINF_lower: "bdd_below (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> \<Sqinter>(f ` A) \<le> f x"
   using cInf_lower [of _ "f ` A"] by simp
 
-lemma cINF_greatest: "A \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> m \<le> f x) \<Longrightarrow> m \<le> INFIMUM A f"
+lemma cINF_greatest: "A \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> m \<le> f x) \<Longrightarrow> m \<le> \<Sqinter>(f ` A)"
   using cInf_greatest [of "f ` A"] by auto
 
-lemma cSUP_upper: "x \<in> A \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> f x \<le> SUPREMUM A f"
+lemma cSUP_upper: "x \<in> A \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> f x \<le> \<Squnion>(f ` A)"
   using cSup_upper [of _ "f ` A"] by simp
 
-lemma cSUP_least: "A \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<le> M) \<Longrightarrow> SUPREMUM A f \<le> M"
+lemma cSUP_least: "A \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<le> M) \<Longrightarrow> \<Squnion>(f ` A) \<le> M"
   using cSup_least [of "f ` A"] by auto
 
-lemma cINF_lower2: "bdd_below (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> f x \<le> u \<Longrightarrow> INFIMUM A f \<le> u"
+lemma cINF_lower2: "bdd_below (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> f x \<le> u \<Longrightarrow> \<Sqinter>(f ` A) \<le> u"
   by (auto intro: cINF_lower order_trans)
 
-lemma cSUP_upper2: "bdd_above (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> u \<le> f x \<Longrightarrow> u \<le> SUPREMUM A f"
+lemma cSUP_upper2: "bdd_above (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> u \<le> f x \<Longrightarrow> u \<le> \<Squnion>(f ` A)"
   by (auto intro: cSUP_upper order_trans)
 
 lemma cSUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Squnion>x\<in>A. c) = c"
@@ -310,10 +310,10 @@
 lemma cINF_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>x\<in>A. c) = c"
   by (intro antisym cINF_greatest) (auto intro: cINF_lower)
 
-lemma le_cINF_iff: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> u \<le> INFIMUM A f \<longleftrightarrow> (\<forall>x\<in>A. u \<le> f x)"
+lemma le_cINF_iff: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> u \<le> \<Sqinter>(f ` A) \<longleftrightarrow> (\<forall>x\<in>A. u \<le> f x)"
   by (metis cINF_greatest cINF_lower order_trans)
 
-lemma cSUP_le_iff: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> SUPREMUM A f \<le> u \<longleftrightarrow> (\<forall>x\<in>A. f x \<le> u)"
+lemma cSUP_le_iff: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> \<Squnion>(f ` A) \<le> u \<longleftrightarrow> (\<forall>x\<in>A. f x \<le> u)"
   by (metis cSUP_least cSUP_upper order_trans)
 
 lemma less_cINF_D: "bdd_below (f`A) \<Longrightarrow> y < (\<Sqinter>i\<in>A. f i) \<Longrightarrow> i \<in> A \<Longrightarrow> y < f i"
@@ -322,22 +322,22 @@
 lemma cSUP_lessD: "bdd_above (f`A) \<Longrightarrow> (\<Squnion>i\<in>A. f i) < y \<Longrightarrow> i \<in> A \<Longrightarrow> f i < y"
   by (metis cSUP_upper le_less_trans)
 
-lemma cINF_insert: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> INFIMUM (insert a A) f = inf (f a) (INFIMUM A f)"
-  by (metis cInf_insert image_insert image_is_empty)
+lemma cINF_insert: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> \<Sqinter>(f ` insert a A) = inf (f a) (\<Sqinter>(f ` A))"
+  by (simp add: cInf_insert cong del: INF_cong)
 
-lemma cSUP_insert: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> SUPREMUM (insert a A) f = sup (f a) (SUPREMUM A f)"
-  by (metis cSup_insert image_insert image_is_empty)
+lemma cSUP_insert: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> \<Squnion>(f ` insert a A) = sup (f a) (\<Squnion>(f ` A))"
+  by (simp add: cSup_insert cong del: SUP_cong)
 
-lemma cINF_mono: "B \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> (\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<le> g m) \<Longrightarrow> INFIMUM A f \<le> INFIMUM B g"
+lemma cINF_mono: "B \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> (\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<le> g m) \<Longrightarrow> \<Sqinter>(f ` A) \<le> \<Sqinter>(g ` B)"
   using cInf_mono [of "g ` B" "f ` A"] by auto
 
-lemma cSUP_mono: "A \<noteq> {} \<Longrightarrow> bdd_above (g ` B) \<Longrightarrow> (\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<le> g m) \<Longrightarrow> SUPREMUM A f \<le> SUPREMUM B g"
+lemma cSUP_mono: "A \<noteq> {} \<Longrightarrow> bdd_above (g ` B) \<Longrightarrow> (\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<le> g m) \<Longrightarrow> \<Squnion>(f ` A) \<le> \<Squnion>(g ` B)"
   using cSup_mono [of "f ` A" "g ` B"] by auto
 
-lemma cINF_superset_mono: "A \<noteq> {} \<Longrightarrow> bdd_below (g ` B) \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> g x \<le> f x) \<Longrightarrow> INFIMUM B g \<le> INFIMUM A f"
+lemma cINF_superset_mono: "A \<noteq> {} \<Longrightarrow> bdd_below (g ` B) \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> g x \<le> f x) \<Longrightarrow> \<Sqinter>(g ` B) \<le> \<Sqinter>(f ` A)"
   by (rule cINF_mono) auto
 
-lemma cSUP_subset_mono: "A \<noteq> {} \<Longrightarrow> bdd_above (g ` B) \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<le> g x) \<Longrightarrow> SUPREMUM A f \<le> SUPREMUM B g"
+lemma cSUP_subset_mono: "A \<noteq> {} \<Longrightarrow> bdd_above (g ` B) \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<le> g x) \<Longrightarrow> \<Squnion>(f ` A) \<le> \<Squnion>(g ` B)"
   by (rule cSUP_mono) auto
 
 lemma less_eq_cInf_inter: "bdd_below A \<Longrightarrow> bdd_below B \<Longrightarrow> A \<inter> B \<noteq> {} \<Longrightarrow> inf (Inf A) (Inf B) \<le> Inf (A \<inter> B)"
@@ -349,20 +349,20 @@
 lemma cInf_union_distrib: "A \<noteq> {} \<Longrightarrow> bdd_below A \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_below B \<Longrightarrow> Inf (A \<union> B) = inf (Inf A) (Inf B)"
   by (intro antisym le_infI cInf_greatest cInf_lower) (auto intro: le_infI1 le_infI2 cInf_lower)
 
-lemma cINF_union: "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_below (f`B) \<Longrightarrow> INFIMUM (A \<union> B) f = inf (INFIMUM A f) (INFIMUM B f)"
-  using cInf_union_distrib [of "f ` A" "f ` B"] by (simp add: image_Un [symmetric])
+lemma cINF_union: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_below (f ` B) \<Longrightarrow> \<Sqinter> (f ` (A \<union> B)) = \<Sqinter> (f ` A) \<sqinter> \<Sqinter> (f ` B)"
+  using cInf_union_distrib [of "f ` A" "f ` B"] by (simp add: image_Un cong del: INF_cong)
 
 lemma cSup_union_distrib: "A \<noteq> {} \<Longrightarrow> bdd_above A \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_above B \<Longrightarrow> Sup (A \<union> B) = sup (Sup A) (Sup B)"
   by (intro antisym le_supI cSup_least cSup_upper) (auto intro: le_supI1 le_supI2 cSup_upper)
 
-lemma cSUP_union: "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_above (f`B) \<Longrightarrow> SUPREMUM (A \<union> B) f = sup (SUPREMUM A f) (SUPREMUM B f)"
-  using cSup_union_distrib [of "f ` A" "f ` B"] by (simp add: image_Un [symmetric])
+lemma cSUP_union: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_above (f ` B) \<Longrightarrow> \<Squnion> (f ` (A \<union> B)) = \<Squnion> (f ` A) \<squnion> \<Squnion> (f ` B)"
+  using cSup_union_distrib [of "f ` A" "f ` B"] by (simp add: image_Un cong del: SUP_cong)
 
-lemma cINF_inf_distrib: "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> bdd_below (g`A) \<Longrightarrow> inf (INFIMUM A f) (INFIMUM A g) = (\<Sqinter>a\<in>A. inf (f a) (g a))"
+lemma cINF_inf_distrib: "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> bdd_below (g`A) \<Longrightarrow> \<Sqinter> (f ` A) \<sqinter> \<Sqinter> (g ` A) = (\<Sqinter>a\<in>A. inf (f a) (g a))"
   by (intro antisym le_infI cINF_greatest cINF_lower2)
      (auto intro: le_infI1 le_infI2 cINF_greatest cINF_lower le_infI)
 
-lemma SUP_sup_distrib: "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> bdd_above (g`A) \<Longrightarrow> sup (SUPREMUM A f) (SUPREMUM A g) = (\<Squnion>a\<in>A. sup (f a) (g a))"
+lemma SUP_sup_distrib: "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> bdd_above (g`A) \<Longrightarrow> \<Squnion> (f ` A) \<squnion> \<Squnion> (g ` A) = (\<Squnion>a\<in>A. sup (f a) (g a))"
   by (intro antisym le_supI cSUP_least cSUP_upper2)
      (auto intro: le_supI1 le_supI2 cSUP_least cSUP_upper le_supI)
 
diff -r ff7e6751a1a7 -r 9bbd5497befd src/HOL/Enum.thy
--- a/src/HOL/Enum.thy	Sat Nov 10 07:57:18 2018 +0000
+++ b/src/HOL/Enum.thy	Sat Nov 10 07:57:19 2018 +0000
@@ -846,8 +846,8 @@
     by simp
 qed
 
-lemma finite_Inf_Sup: "INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
-proof (rule  finite_induct [of A "\<lambda> A .INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"], simp_all add: finite_UnionD)
+lemma finite_Inf_Sup: "\<Sqinter>(Sup ` A) \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
+proof (rule finite_induct [of A "\<lambda>A. \<Sqinter>(Sup ` A) \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"], simp_all add: finite_UnionD)
   fix x::"'a set"
   fix F
   assume "x \<notin> F"
@@ -858,13 +858,13 @@
     by (auto simp add: fa_def)
   from this have B: "\<And>f b. \<forall>Y\<in>F. f Y \<in> Y \<Longrightarrow> b \<in> x \<Longrightarrow> fa b f ` ({x} \<union> F) \<in> {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)}"
     by blast
-  have [simp]: "\<And>f b. \<forall>Y\<in>F. f Y \<in> Y \<Longrightarrow> b \<in> x \<Longrightarrow> b \<sqinter> (\<Sqinter>x\<in>F. f x)  \<le> SUPREMUM {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)} Inf"
+  have [simp]: "\<And>f b. \<forall>Y\<in>F. f Y \<in> Y \<Longrightarrow> b \<in> x \<Longrightarrow> b \<sqinter> (\<Sqinter>x\<in>F. f x)  \<le> \<Squnion>(Inf ` {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)})"
     using B apply (rule SUP_upper2, simp_all)
     by (simp_all add: INF_greatest Inf_lower inf.coboundedI2 fa_def)
 
-  assume "INFIMUM F Sup \<le> SUPREMUM {f ` F |f. \<forall>Y\<in>F. f Y \<in> Y} Inf"
+  assume "\<Sqinter>(Sup ` F) \<le> \<Squnion>(Inf ` {f ` F |f. \<forall>Y\<in>F. f Y \<in> Y})"
 
-  from this have "\<Squnion>x \<sqinter> INFIMUM F Sup \<le> \<Squnion>x \<sqinter> SUPREMUM {f ` F |f. \<forall>Y\<in>F. f Y \<in> Y} Inf"
+  from this have "\<Squnion>x \<sqinter> \<Sqinter>(Sup ` F) \<le> \<Squnion>x \<sqinter> \<Squnion>(Inf ` {f ` F |f. \<forall>Y\<in>F. f Y \<in> Y})"
     apply simp
     using inf.coboundedI2 by blast
   also have "... = Sup {\<Squnion>x \<sqinter> (Inf (f ` F)) |f  .  (\<forall>Y\<in>F. f Y \<in> Y)}"
@@ -874,11 +874,11 @@
     apply (subst inf_commute)
     by (simp add: finite_inf_Sup)
 
-  also have "... \<le> SUPREMUM {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)} Inf"
+  also have "... \<le> \<Squnion>(Inf ` {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)})"
     apply (rule Sup_least, clarsimp)+
     by (subst inf_commute, simp)
 
-  finally show "\<Squnion>x \<sqinter> INFIMUM F Sup \<le> SUPREMUM {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)} Inf"
+  finally show "\<Squnion>x \<sqinter> \<Sqinter>(Sup ` F) \<le> \<Squnion>(Inf ` {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)})"
     by simp
 qed
 
diff -r ff7e6751a1a7 -r 9bbd5497befd src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Sat Nov 10 07:57:18 2018 +0000
+++ b/src/HOL/Filter.thy	Sat Nov 10 07:57:19 2018 +0000
@@ -669,9 +669,9 @@
       by (subst eventually_INF) blast
     also have "\<dots> \<longleftrightarrow> (\<exists>X. (X \<subseteq> B \<and> finite X) \<and> eventually P (filtercomap f (\<Sqinter>b\<in>X. F b)))"
       by (rule ex_cong) (simp add: *)
-    also have "\<dots> \<longleftrightarrow> eventually P (filtercomap f (INFIMUM B F))"
+    also have "\<dots> \<longleftrightarrow> eventually P (filtercomap f (\<Sqinter>(F ` B)))"
       unfolding eventually_filtercomap by (subst eventually_INF) blast
-    finally show "eventually P (filtercomap f (INFIMUM B F)) = 
+    finally show "eventually P (filtercomap f (\<Sqinter>(F ` B))) = 
                     eventually P (\<Sqinter>b\<in>B. filtercomap f (F b))" ..
   qed
 qed
diff -r ff7e6751a1a7 -r 9bbd5497befd src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sat Nov 10 07:57:18 2018 +0000
+++ b/src/HOL/Finite_Set.thy	Sat Nov 10 07:57:19 2018 +0000
@@ -256,7 +256,7 @@
   "finite A \<Longrightarrow> (\<And>a. a \<in> A \<Longrightarrow> finite (B a)) \<Longrightarrow> finite (\<Union>a\<in>A. B a)"
   by (induct rule: finite_induct) simp_all
 
-lemma finite_UN [simp]: "finite A \<Longrightarrow> finite (UNION A B) \<longleftrightarrow> (\<forall>x\<in>A. finite (B x))"
+lemma finite_UN [simp]: "finite A \<Longrightarrow> finite (\<Union>(B ` A)) \<longleftrightarrow> (\<forall>x\<in>A. finite (B x))"
   by (blast intro: finite_subset)
 
 lemma finite_Inter [intro]: "\<exists>A\<in>M. finite A \<Longrightarrow> finite (\<Inter>M)"
@@ -1254,7 +1254,7 @@
 
 lemma inf_INF_fold_inf:
   assumes "finite A"
-  shows "inf B (INFIMUM A f) = fold (inf \<circ> f) B A" (is "?inf = ?fold")
+  shows "inf B (\<Sqinter>(f ` A)) = fold (inf \<circ> f) B A" (is "?inf = ?fold")
 proof -
   interpret comp_fun_idem inf by (fact comp_fun_idem_inf)
   interpret comp_fun_idem "inf \<circ> f" by (fact comp_comp_fun_idem)
@@ -1265,7 +1265,7 @@
 
 lemma sup_SUP_fold_sup:
   assumes "finite A"
-  shows "sup B (SUPREMUM A f) = fold (sup \<circ> f) B A" (is "?sup = ?fold")
+  shows "sup B (\<Squnion>(f ` A)) = fold (sup \<circ> f) B A" (is "?sup = ?fold")
 proof -
   interpret comp_fun_idem sup by (fact comp_fun_idem_sup)
   interpret comp_fun_idem "sup \<circ> f" by (fact comp_comp_fun_idem)
@@ -1274,10 +1274,10 @@
   then show ?thesis ..
 qed
 
-lemma INF_fold_inf: "finite A \<Longrightarrow> INFIMUM A f = fold (inf \<circ> f) top A"
+lemma INF_fold_inf: "finite A \<Longrightarrow> \<Sqinter>(f ` A) = fold (inf \<circ> f) top A"
   using inf_INF_fold_inf [of A top] by simp
 
-lemma SUP_fold_sup: "finite A \<Longrightarrow> SUPREMUM A f = fold (sup \<circ> f) bot A"
+lemma SUP_fold_sup: "finite A \<Longrightarrow> \<Squnion>(f ` A) = fold (sup \<circ> f) bot A"
   using sup_SUP_fold_sup [of A bot] by simp
 
 end
diff -r ff7e6751a1a7 -r 9bbd5497befd src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Sat Nov 10 07:57:18 2018 +0000
+++ b/src/HOL/Groups_Big.thy	Sat Nov 10 07:57:19 2018 +0000
@@ -161,14 +161,14 @@
 lemma UNION_disjoint:
   assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
     and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
-  shows "F g (UNION I A) = F (\<lambda>x. F g (A x)) I"
+  shows "F g (\<Union>(A ` I)) = F (\<lambda>x. F g (A x)) I"
   apply (insert assms)
   apply (induct rule: finite_induct)
    apply simp
   apply atomize
   apply (subgoal_tac "\<forall>i\<in>Fa. x \<noteq> i")
    prefer 2 apply blast
-  apply (subgoal_tac "A x \<inter> UNION Fa A = {}")
+  apply (subgoal_tac "A x \<inter> \<Union>(A ` Fa) = {}")
    prefer 2 apply blast
   apply (simp add: union_disjoint)
   done
@@ -1023,7 +1023,7 @@
 lemma card_UN_disjoint:
   assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
     and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
-  shows "card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
+  shows "card (\<Union>(A ` I)) = (\<Sum>i\<in>I. card(A i))"
 proof -
   have "(\<Sum>i\<in>I. card (A i)) = (\<Sum>i\<in>I. \<Sum>x\<in>A i. 1)"
     by simp
diff -r ff7e6751a1a7 -r 9bbd5497befd src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Sat Nov 10 07:57:18 2018 +0000
+++ b/src/HOL/Hilbert_Choice.thy	Sat Nov 10 07:57:19 2018 +0000
@@ -911,39 +911,39 @@
 begin
 lemma Sup_Inf: "Sup (Inf ` A) = Inf (Sup ` {f ` A | f . (\<forall> Y \<in> A . f Y \<in> Y)})"
 proof (rule antisym)
-  show "SUPREMUM A Inf \<le> INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Sup"
+  show "\<Squnion>(Inf ` A) \<le> \<Sqinter>(Sup ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
     apply (rule Sup_least, rule INF_greatest)
     using Inf_lower2 Sup_upper by auto
 next
-  show "INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Sup \<le> SUPREMUM A Inf"
+  show "\<Sqinter>(Sup ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> \<Squnion>(Inf ` A)"
   proof (simp add:  Inf_Sup, rule SUP_least, simp, safe)
     fix f
     assume "\<forall>Y. (\<exists>f. Y = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<longrightarrow> f Y \<in> Y"
     from this have B: "\<And> F . (\<forall> Y \<in> A . F Y \<in> Y) \<Longrightarrow> \<exists> Z \<in> A . f (F ` A) = F Z"
       by auto
-    show "INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> SUPREMUM A Inf"
-    proof (cases "\<exists> Z \<in> A . INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> Inf Z")
+    show "\<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> \<Squnion>(Inf ` A)"
+    proof (cases "\<exists> Z \<in> A . \<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> Inf Z")
       case True
-      from this obtain Z where [simp]: "Z \<in> A" and A: "INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> Inf Z"
+      from this obtain Z where [simp]: "Z \<in> A" and A: "\<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> Inf Z"
         by blast
-      have B: "... \<le> SUPREMUM A Inf"
+      have B: "... \<le> \<Squnion>(Inf ` A)"
         by (simp add: SUP_upper)
       from A and B show ?thesis
         by simp
     next
       case False
-      from this have X: "\<And> Z . Z \<in> A \<Longrightarrow> \<exists> x . x \<in> Z \<and> \<not> INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> x"
+      from this have X: "\<And> Z . Z \<in> A \<Longrightarrow> \<exists> x . x \<in> Z \<and> \<not> \<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> x"
         using Inf_greatest by blast
-      define F where "F = (\<lambda> Z . SOME x . x \<in> Z \<and> \<not> INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> x)"
+      define F where "F = (\<lambda> Z . SOME x . x \<in> Z \<and> \<not> \<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> x)"
       have C: "\<And> Y . Y \<in> A \<Longrightarrow> F Y \<in> Y"
         using X by (simp add: F_def, rule someI2_ex, auto)
-      have E: "\<And> Y . Y \<in> A \<Longrightarrow> \<not> INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> F Y"
+      have E: "\<And> Y . Y \<in> A \<Longrightarrow> \<not> \<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> F Y"
         using X by (simp add: F_def, rule someI2_ex, auto)
       from C and B obtain  Z where D: "Z \<in> A " and Y: "f (F ` A) = F Z"
         by blast
-      from E and D have W: "\<not> INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> F Z"
+      from E and D have W: "\<not> \<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> F Z"
         by simp
-      have "INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> f (F ` A)"
+      have "\<Sqinter>(f ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) \<le> f (F ` A)"
         apply (rule INF_lower)
         using C by blast
       from this and W and Y show ?thesis
@@ -966,7 +966,7 @@
 next
   have "\<Sqinter>((\<squnion>) a ` B) \<le> \<Sqinter>(Sup ` {{f {a}, f B} |f. f {a} = a \<and> f B \<in> B})"
     by (rule INF_greatest, auto simp add: INF_lower)
-  also have "... = SUPREMUM {{a}, B} Inf"
+  also have "... = \<Squnion>(Inf ` {{a}, B})"
     by (unfold Sup_Inf, simp)
   finally show "\<Sqinter>((\<squnion>) a ` B) \<le> a \<squnion> \<Sqinter>B"
     by simp
@@ -1024,7 +1024,7 @@
     by (rule INF_lower2, blast+)
   have B: "\<And>f xa. \<forall>Y\<in>A. f Y \<in> Y \<Longrightarrow> xa \<in> A \<Longrightarrow> f xa \<in> xa"
     by blast
-  have A: "\<And>f xa. \<forall>Y\<in>A. f Y \<in> Y \<Longrightarrow> xa \<in> A \<Longrightarrow> (\<Sqinter>x\<in>A. g (f x)) \<le> SUPREMUM xa g"
+  have A: "\<And>f xa. \<forall>Y\<in>A. f Y \<in> Y \<Longrightarrow> xa \<in> A \<Longrightarrow> (\<Sqinter>x\<in>A. g (f x)) \<le> \<Squnion>(g ` xa)"
     by (rule SUP_upper2, rule B, simp_all, simp)
   show "(\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>a\<in>x. g a) \<le> (\<Sqinter>x\<in>A. \<Squnion>a\<in>x. g a)"
     apply (rule SUP_least, simp, safe, rule INF_greatest, simp)
@@ -1175,13 +1175,13 @@
 subclass complete_distrib_lattice
 proof (standard, rule ccontr)
   fix A
-  assume "\<not> INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
-  from this have C: "INFIMUM A Sup > SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
-    using local.not_le by blast
-  show "False"
-    proof (cases "\<exists> z . INFIMUM A Sup > z \<and> z > SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf")
+  assume "\<not> \<Sqinter>(Sup ` A) \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
+  then have C: "\<Sqinter>(Sup ` A) > \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
+    by (simp add: not_le)
+  show False
+    proof (cases "\<exists> z . \<Sqinter>(Sup ` A) > z \<and> z > \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})")
       case True
-      from this obtain z where A: "z < INFIMUM A Sup" and X: "SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf < z"
+      from this obtain z where A: "z < \<Sqinter>(Sup ` A)" and X: "z > \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
         by blast
           
       from A have "\<And> Y . Y \<in> A \<Longrightarrow> z < Sup Y"
@@ -1204,28 +1204,28 @@
       have "z \<le> Inf (F ` A)"
         by (simp add: D local.INF_greatest local.order.strict_implies_order)
     
-      also have "... \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
+      also have "... \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
         apply (rule SUP_upper, safe)
         using E by blast
-      finally have "z \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
+      finally have "z \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
         by simp
           
       from X and this show ?thesis
         using local.not_less by blast
     next
       case False
-      from this have A: "\<And> z . INFIMUM A Sup \<le> z \<or> z \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
+      from this have A: "\<And> z . \<Sqinter>(Sup ` A) \<le> z \<or> z \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
         using local.le_less_linear by blast
-          
-      from C have "\<And> Y . Y \<in> A \<Longrightarrow> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf < Sup Y"
+
+      from C have "\<And> Y . Y \<in> A \<Longrightarrow> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) < Sup Y"
         by (simp add: less_INF_D)
-    
-      from this have B: "\<And> Y . Y \<in> A \<Longrightarrow> \<exists> k \<in>Y . SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf < k"
+
+      from this have B: "\<And> Y . Y \<in> A \<Longrightarrow> \<exists> k \<in>Y . \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) < k"
         using local.less_Sup_iff by blast
           
-      define F where "F = (\<lambda> Y . SOME k . k \<in> Y \<and> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf < k)"
-        
-      have D: "\<And> Y . Y \<in> A \<Longrightarrow> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf < F Y"
+      define F where "F = (\<lambda> Y . SOME k . k \<in> Y \<and> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) < k)"
+
+      have D: "\<And> Y . Y \<in> A \<Longrightarrow> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}) < F Y"
         using B apply (simp add: F_def)
         by (rule someI2_ex, auto)
     
@@ -1233,17 +1233,17 @@
         using B apply (simp add: F_def)
         by (rule someI2_ex, auto)
           
-      have "\<And> Y . Y \<in> A \<Longrightarrow> INFIMUM A Sup \<le> F Y"
+      have "\<And> Y . Y \<in> A \<Longrightarrow> \<Sqinter>(Sup ` A) \<le> F Y"
         using D False local.leI by blast
          
-      from this have "INFIMUM A Sup \<le> Inf (F ` A)"
+      from this have "\<Sqinter>(Sup ` A) \<le> Inf (F ` A)"
         by (simp add: local.INF_greatest)
           
-      also have "Inf (F ` A) \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
+      also have "Inf (F ` A) \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
         apply (rule SUP_upper, safe)
         using E by blast
-          
-      finally have "INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
+
+      finally have "\<Sqinter>(Sup ` A) \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
         by simp
         
       from C and this show ?thesis
diff -r ff7e6751a1a7 -r 9bbd5497befd src/HOL/Lifting_Set.thy
--- a/src/HOL/Lifting_Set.thy	Sat Nov 10 07:57:18 2018 +0000
+++ b/src/HOL/Lifting_Set.thy	Sat Nov 10 07:57:19 2018 +0000
@@ -134,8 +134,8 @@
   "((A ===> B) ===> rel_set A ===> rel_set B) image image"
   unfolding rel_fun_def rel_set_def by simp fast
 
-lemma UNION_transfer [transfer_rule]:
-  "(rel_set A ===> (A ===> rel_set B) ===> rel_set B) UNION UNION"
+lemma UNION_transfer [transfer_rule]: \<comment> \<open>TODO deletion candidate\<close>
+  "(rel_set A ===> (A ===> rel_set B) ===> rel_set B) (\<lambda>A f. \<Union>(f ` A)) (\<lambda>A f. \<Union>(f ` A))"
   by transfer_prover
 
 lemma Ball_transfer [transfer_rule]:
@@ -172,12 +172,12 @@
   "(rel_set A ===> (A ===> rel_set B) ===> rel_set B) Set.bind Set.bind"
   unfolding bind_UNION [abs_def] by transfer_prover
 
-lemma INF_parametric [transfer_rule]:
-  "(rel_set A ===> (A ===> HOL.eq) ===> HOL.eq) INFIMUM INFIMUM"
+lemma INF_parametric [transfer_rule]: \<comment> \<open>TODO deletion candidate\<close>
+  "(rel_set A ===> (A ===> HOL.eq) ===> HOL.eq) (\<lambda>A f. Inf (f ` A)) (\<lambda>A f. Inf (f ` A))"
   by transfer_prover
 
-lemma SUP_parametric [transfer_rule]:
-  "(rel_set R ===> (R ===> HOL.eq) ===> HOL.eq) SUPREMUM SUPREMUM"
+lemma SUP_parametric [transfer_rule]: \<comment> \<open>TODO deletion candidate\<close>
+  "(rel_set R ===> (R ===> HOL.eq) ===> HOL.eq) (\<lambda>A f. Sup (f ` A)) (\<lambda>A f. Sup (f ` A))"
   by transfer_prover
 
 
@@ -316,7 +316,7 @@
 
 lemma rel_set_UNION:
   assumes [transfer_rule]: "rel_set Q A B" "rel_fun Q (rel_set R) f g"
-  shows "rel_set R (UNION A f) (UNION B g)"
+  shows "rel_set R (\<Union>(f ` A)) (\<Union>(g ` B))"
   by transfer_prover
 
 end
diff -r ff7e6751a1a7 -r 9bbd5497befd src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Nov 10 07:57:18 2018 +0000
+++ b/src/HOL/List.thy	Sat Nov 10 07:57:19 2018 +0000
@@ -2985,11 +2985,11 @@
 declare Sup_set_fold [where 'a = "'a set", code]
 
 lemma (in complete_lattice) INF_set_fold:
-  "INFIMUM (set xs) f = fold (inf \<circ> f) xs top"
+  "\<Sqinter>(f ` set xs) = fold (inf \<circ> f) xs top"
   using Inf_set_fold [of "map f xs"] by (simp add: fold_map)
 
 lemma (in complete_lattice) SUP_set_fold:
-  "SUPREMUM (set xs) f = fold (sup \<circ> f) xs bot"
+  "\<Squnion>(f ` set xs) = fold (sup \<circ> f) xs bot"
   using Sup_set_fold [of "map f xs"] by (simp add: fold_map)
 
 
diff -r ff7e6751a1a7 -r 9bbd5497befd src/HOL/Main.thy
--- a/src/HOL/Main.thy	Sat Nov 10 07:57:18 2018 +0000
+++ b/src/HOL/Main.thy	Sat Nov 10 07:57:19 2018 +0000
@@ -11,12 +11,50 @@
     Quickcheck_Narrowing 
     Extraction
     Nunchaku
-    BNF_Greatest_Fixpoint Filter
+    BNF_Greatest_Fixpoint
+    Filter
     Conditionally_Complete_Lattices
     Binomial
     GCD
 begin
 
+text \<open>Legacy\<close>
+
+context Inf
+begin
+
+abbreviation (input) INFIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
+  where "INFIMUM A f \<equiv> \<Sqinter>(f ` A)"
+
+end
+
+context Sup
+begin
+
+abbreviation (input) SUPREMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
+  where "SUPREMUM A f \<equiv> \<Squnion>(f ` A)"
+
+end
+
+abbreviation (input) INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
+  where "INTER \<equiv> INFIMUM"
+
+abbreviation (input) UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
+  where "UNION \<equiv> SUPREMUM"
+
+
+text \<open>Namespace cleanup\<close>
+
+hide_const (open)
+  czero cinfinite cfinite csum cone ctwo Csum cprod cexp image2 image2p vimage2p Gr Grp collect
+  fsts snds setl setr convol pick_middlep fstOp sndOp csquare relImage relInvImage Succ Shift
+  shift proj id_bnf
+
+hide_fact (open) id_bnf_def type_definition_id_bnf_UNIV
+
+
+text \<open>Syntax cleanup\<close>
+
 no_notation
   bot ("\<bottom>") and
   top ("\<top>") and
@@ -29,17 +67,10 @@
   ordLess2 (infix "<o" 50) and
   ordIso2 (infix "=o" 50) and
   card_of ("|_|") and
-  csum (infixr "+c" 65) and
-  cprod (infixr "*c" 80) and
-  cexp (infixr "^c" 90) and
-  convol ("\<langle>(_,/ _)\<rangle>")
-
-hide_const (open)
-  czero cinfinite cfinite csum cone ctwo Csum cprod cexp image2 image2p vimage2p Gr Grp collect
-  fsts snds setl setr convol pick_middlep fstOp sndOp csquare relImage relInvImage Succ Shift
-  shift proj id_bnf
-
-hide_fact (open) id_bnf_def type_definition_id_bnf_UNIV
+  BNF_Cardinal_Arithmetic.csum (infixr "+c" 65) and
+  BNF_Cardinal_Arithmetic.cprod (infixr "*c" 80) and
+  BNF_Cardinal_Arithmetic.cexp (infixr "^c" 90) and
+  BNF_Def.convol ("\<langle>(_,/ _)\<rangle>")
 
 no_syntax
   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
diff -r ff7e6751a1a7 -r 9bbd5497befd src/HOL/Option.thy
--- a/src/HOL/Option.thy	Sat Nov 10 07:57:18 2018 +0000
+++ b/src/HOL/Option.thy	Sat Nov 10 07:57:19 2018 +0000
@@ -260,7 +260,7 @@
 lemma bind_map_option: "bind (map_option f x) g = bind x (g \<circ> f)"
 by(cases x) simp_all
 
-lemma set_bind_option [simp]: "set_option (bind x f) = UNION (set_option x) (set_option \<circ> f)"
+lemma set_bind_option [simp]: "set_option (bind x f) = (\<Union>((set_option \<circ> f) ` set_option x))"
 by(cases x) auto
 
 lemma map_conv_bind_option: "map_option f x = Option.bind x (Some \<circ> f)"
diff -r ff7e6751a1a7 -r 9bbd5497befd src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Sat Nov 10 07:57:18 2018 +0000
+++ b/src/HOL/Predicate.thy	Sat Nov 10 07:57:19 2018 +0000
@@ -58,17 +58,17 @@
   by (simp add: sup_pred_def)
 
 definition
-  "\<Sqinter>A = Pred (INFIMUM A eval)"
+  "\<Sqinter>A = Pred (\<Sqinter>(eval ` A))"
 
 lemma eval_Inf [simp]:
-  "eval (\<Sqinter>A) = INFIMUM A eval"
+  "eval (\<Sqinter>A) = \<Sqinter>(eval ` A)"
   by (simp add: Inf_pred_def)
 
 definition
-  "\<Squnion>A = Pred (SUPREMUM A eval)"
+  "\<Squnion>A = Pred (\<Squnion>(eval ` A))"
 
 lemma eval_Sup [simp]:
-  "eval (\<Squnion>A) = SUPREMUM A eval"
+  "eval (\<Squnion>A) = \<Squnion>(eval ` A)"
   by (simp add: Sup_pred_def)
 
 instance proof
@@ -77,12 +77,12 @@
 end
 
 lemma eval_INF [simp]:
-  "eval (INFIMUM A f) = INFIMUM A (eval \<circ> f)"
-  using eval_Inf [of "f ` A"] by simp
+  "eval (\<Sqinter>(f ` A)) = \<Sqinter>((eval \<circ> f) ` A)"
+  by simp
 
 lemma eval_SUP [simp]:
-  "eval (SUPREMUM A f) = SUPREMUM A (eval \<circ> f)"
-  using eval_Sup [of "f ` A"] by simp
+  "eval (\<Squnion>(f ` A)) = \<Squnion>((eval \<circ> f) ` A)"
+  by simp
 
 instantiation pred :: (type) complete_boolean_algebra
 begin
@@ -103,7 +103,7 @@
 
 instance proof
   fix A::"'a pred set set"
-  show "INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
+  show "\<Sqinter>(Sup ` A) \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
   proof (simp add: less_eq_pred_def Sup_fun_def Inf_fun_def, safe)
     fix w
     assume A: "\<forall>x\<in>A. \<exists>f\<in>x. eval f w"
@@ -127,10 +127,10 @@
   by (simp add: single_def)
 
 definition bind :: "'a pred \<Rightarrow> ('a \<Rightarrow> 'b pred) \<Rightarrow> 'b pred" (infixl "\<bind>" 70) where
-  "P \<bind> f = (SUPREMUM {x. eval P x} f)"
+  "P \<bind> f = (\<Squnion>(f ` {x. eval P x}))"
 
 lemma eval_bind [simp]:
-  "eval (P \<bind> f) = eval (SUPREMUM {x. eval P x} f)"
+  "eval (P \<bind> f) = eval (\<Squnion>(f ` {x. eval P x}))"
   by (simp add: bind_def)
 
 lemma bind_bind:
diff -r ff7e6751a1a7 -r 9bbd5497befd src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Sat Nov 10 07:57:18 2018 +0000
+++ b/src/HOL/Product_Type.thy	Sat Nov 10 07:57:19 2018 +0000
@@ -1049,7 +1049,7 @@
     \<Longrightarrow> A \<subseteq> Collect (case_prod P) \<Longrightarrow> A \<subseteq> Collect (case_prod Q)"
   by fastforce
 
-lemma UN_Times_distrib: "(\<Union>(a, b)\<in>A \<times> B. E a \<times> F b) = UNION A E \<times> UNION B F"
+lemma UN_Times_distrib: "(\<Union>(a, b)\<in>A \<times> B. E a \<times> F b) = \<Union>(E ` A) \<times> \<Union>(F ` B)"
   \<comment> \<open>Suggested by Pierre Chartier\<close>
   by blast
 
diff -r ff7e6751a1a7 -r 9bbd5497befd src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Sat Nov 10 07:57:18 2018 +0000
+++ b/src/HOL/Relation.thy	Sat Nov 10 07:57:19 2018 +0000
@@ -120,25 +120,25 @@
 lemma SUP_UN_eq2 [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Union>i\<in>S. r i))"
   by (simp add: fun_eq_iff)
 
-lemma Inf_INT_eq [pred_set_conv]: "\<Sqinter>S = (\<lambda>x. x \<in> INTER S Collect)"
+lemma Inf_INT_eq [pred_set_conv]: "\<Sqinter>S = (\<lambda>x. x \<in> (\<Inter>(Collect ` S)))"
   by (simp add: fun_eq_iff)
 
 lemma INF_Int_eq [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x. x \<in> i)) = (\<lambda>x. x \<in> \<Inter>S)"
   by (simp add: fun_eq_iff)
 
-lemma Inf_INT_eq2 [pred_set_conv]: "\<Sqinter>S = (\<lambda>x y. (x, y) \<in> INTER (case_prod ` S) Collect)"
+lemma Inf_INT_eq2 [pred_set_conv]: "\<Sqinter>S = (\<lambda>x y. (x, y) \<in> (\<Inter>(Collect ` case_prod ` S)))"
   by (simp add: fun_eq_iff)
 
 lemma INF_Int_eq2 [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x y. (x, y) \<in> i)) = (\<lambda>x y. (x, y) \<in> \<Inter>S)"
   by (simp add: fun_eq_iff)
 
-lemma Sup_SUP_eq [pred_set_conv]: "\<Squnion>S = (\<lambda>x. x \<in> UNION S Collect)"
+lemma Sup_SUP_eq [pred_set_conv]: "\<Squnion>S = (\<lambda>x. x \<in> \<Union>(Collect ` S))"
   by (simp add: fun_eq_iff)
 
 lemma SUP_Sup_eq [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x. x \<in> i)) = (\<lambda>x. x \<in> \<Union>S)"
   by (simp add: fun_eq_iff)
 
-lemma Sup_SUP_eq2 [pred_set_conv]: "\<Squnion>S = (\<lambda>x y. (x, y) \<in> UNION (case_prod ` S) Collect)"
+lemma Sup_SUP_eq2 [pred_set_conv]: "\<Squnion>S = (\<lambda>x y. (x, y) \<in> (\<Union>(Collect ` case_prod ` S)))"
   by (simp add: fun_eq_iff)
 
 lemma SUP_Sup_eq2 [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x y. (x, y) \<in> i)) = (\<lambda>x y. (x, y) \<in> \<Union>S)"
@@ -198,10 +198,10 @@
 lemma reflp_sup: "reflp r \<Longrightarrow> reflp s \<Longrightarrow> reflp (r \<squnion> s)"
   by (auto intro: reflpI elim: reflpE)
 
-lemma refl_on_INTER: "\<forall>x\<in>S. refl_on (A x) (r x) \<Longrightarrow> refl_on (INTER S A) (INTER S r)"
+lemma refl_on_INTER: "\<forall>x\<in>S. refl_on (A x) (r x) \<Longrightarrow> refl_on (\<Inter>(A ` S)) (\<Inter>(r ` S))"
   unfolding refl_on_def by fast
 
-lemma refl_on_UNION: "\<forall>x\<in>S. refl_on (A x) (r x) \<Longrightarrow> refl_on (UNION S A) (UNION S r)"
+lemma refl_on_UNION: "\<forall>x\<in>S. refl_on (A x) (r x) \<Longrightarrow> refl_on (\<Union>(A ` S)) (\<Union>(r ` S))"
   unfolding refl_on_def by blast
 
 lemma refl_on_empty [simp]: "refl_on {} {}"
@@ -303,16 +303,16 @@
 lemma symp_sup: "symp r \<Longrightarrow> symp s \<Longrightarrow> symp (r \<squnion> s)"
   by (fact sym_Un [to_pred])
 
-lemma sym_INTER: "\<forall>x\<in>S. sym (r x) \<Longrightarrow> sym (INTER S r)"
+lemma sym_INTER: "\<forall>x\<in>S. sym (r x) \<Longrightarrow> sym (\<Inter>(r ` S))"
   by (fast intro: symI elim: symE)
 
-lemma symp_INF: "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (INFIMUM S r)"
+lemma symp_INF: "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (\<Sqinter>(r ` S))"
   by (fact sym_INTER [to_pred])
 
-lemma sym_UNION: "\<forall>x\<in>S. sym (r x) \<Longrightarrow> sym (UNION S r)"
+lemma sym_UNION: "\<forall>x\<in>S. sym (r x) \<Longrightarrow> sym (\<Union>(r ` S))"
   by (fast intro: symI elim: symE)
 
-lemma symp_SUP: "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (SUPREMUM S r)"
+lemma symp_SUP: "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (\<Squnion>(r ` S))"
   by (fact sym_UNION [to_pred])
 
 
@@ -411,10 +411,10 @@
 lemma transp_inf: "transp r \<Longrightarrow> transp s \<Longrightarrow> transp (r \<sqinter> s)"
   by (fact trans_Int [to_pred])
 
-lemma trans_INTER: "\<forall>x\<in>S. trans (r x) \<Longrightarrow> trans (INTER S r)"
+lemma trans_INTER: "\<forall>x\<in>S. trans (r x) \<Longrightarrow> trans (\<Inter>(r ` S))"
   by (fast intro: transI elim: transD)
 
-lemma transp_INF: "\<forall>x\<in>S. transp (r x) \<Longrightarrow> transp (INFIMUM S r)"
+lemma transp_INF: "\<forall>x\<in>S. transp (r x) \<Longrightarrow> transp (\<Sqinter>(r ` S))"
   by (fact trans_INTER [to_pred])
     
 lemma trans_join [code]: "trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)"
@@ -683,16 +683,16 @@
 lemma relcompp_distrib2 [simp]: "(S \<squnion> T) OO R = S OO R \<squnion> T OO R"
   by (fact relcomp_distrib2 [to_pred])
 
-lemma relcomp_UNION_distrib: "s O UNION I r = (\<Union>i\<in>I. s O r i) "
+lemma relcomp_UNION_distrib: "s O \<Union>(r ` I) = (\<Union>i\<in>I. s O r i) "
   by auto
 
-lemma relcompp_SUP_distrib: "s OO SUPREMUM I r = (\<Squnion>i\<in>I. s OO r i)"
+lemma relcompp_SUP_distrib: "s OO \<Squnion>(r ` I) = (\<Squnion>i\<in>I. s OO r i)"
   by (fact relcomp_UNION_distrib [to_pred])
     
-lemma relcomp_UNION_distrib2: "UNION I r O s = (\<Union>i\<in>I. r i O s) "
+lemma relcomp_UNION_distrib2: "\<Union>(r ` I) O s = (\<Union>i\<in>I. r i O s) "
   by auto
 
-lemma relcompp_SUP_distrib2: "SUPREMUM I r OO s = (\<Squnion>i\<in>I. r i OO s)"
+lemma relcompp_SUP_distrib2: "\<Squnion>(r ` I) OO s = (\<Squnion>i\<in>I. r i OO s)"
   by (fact relcomp_UNION_distrib2 [to_pred])
     
 lemma single_valued_relcomp: "single_valued r \<Longrightarrow> single_valued s \<Longrightarrow> single_valued (r O s)"
@@ -781,10 +781,10 @@
 lemma converse_join: "(r \<squnion> s)\<inverse>\<inverse> = r\<inverse>\<inverse> \<squnion> s\<inverse>\<inverse>"
   by (simp add: sup_fun_def) (iprover intro: conversepI ext dest: conversepD)
 
-lemma converse_INTER: "(INTER S r)\<inverse> = (INT x:S. (r x)\<inverse>)"
+lemma converse_INTER: "(\<Inter>(r ` S))\<inverse> = (\<Inter>x\<in>S. (r x)\<inverse>)"
   by fast
 
-lemma converse_UNION: "(UNION S r)\<inverse> = (UN x:S. (r x)\<inverse>)"
+lemma converse_UNION: "(\<Union>(r ` S))\<inverse> = (\<Union>x\<in>S. (r x)\<inverse>)"
   by blast
 
 lemma converse_mono[simp]: "r\<inverse> \<subseteq> s \<inverse> \<longleftrightarrow> r \<subseteq> s"
@@ -1078,17 +1078,17 @@
 lemma Image_mono: "r' \<subseteq> r \<Longrightarrow> A' \<subseteq> A \<Longrightarrow> (r' `` A') \<subseteq> (r `` A)"
   by blast
 
-lemma Image_UN: "(r `` (UNION A B)) = (\<Union>x\<in>A. r `` (B x))"
+lemma Image_UN: "r `` (\<Union>(B ` A)) = (\<Union>x\<in>A. r `` (B x))"
   by blast
 
 lemma UN_Image: "(\<Union>i\<in>I. X i) `` S = (\<Union>i\<in>I. X i `` S)"
   by auto
 
-lemma Image_INT_subset: "(r `` INTER A B) \<subseteq> (\<Inter>x\<in>A. r `` (B x))"
+lemma Image_INT_subset: "(r `` (\<Inter>(B ` A))) \<subseteq> (\<Inter>x\<in>A. r `` (B x))"
   by blast
 
 text \<open>Converse inclusion requires some assumptions\<close>
-lemma Image_INT_eq: "single_valued (r\<inverse>) \<Longrightarrow> A \<noteq> {} \<Longrightarrow> r `` INTER A B = (\<Inter>x\<in>A. r `` B x)"
+lemma Image_INT_eq: "single_valued (r\<inverse>) \<Longrightarrow> A \<noteq> {} \<Longrightarrow> r `` (\<Inter>(B ` A)) = (\<Inter>x\<in>A. r `` B x)"
   apply (rule equalityI)
    apply (rule Image_INT_subset)
   apply (auto simp add: single_valued_def)
diff -r ff7e6751a1a7 -r 9bbd5497befd src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Sat Nov 10 07:57:18 2018 +0000
+++ b/src/HOL/Wellfounded.thy	Sat Nov 10 07:57:19 2018 +0000
@@ -325,7 +325,7 @@
 proof clarify
   fix A and a :: "'b"
   assume "a \<in> A"
-  show "\<exists>z\<in>A. \<forall>y. (y, z) \<in> UNION I r \<longrightarrow> y \<notin> A"
+  show "\<exists>z\<in>A. \<forall>y. (y, z) \<in> \<Union>(r ` I) \<longrightarrow> y \<notin> A"
   proof (cases "\<exists>i\<in>I. \<exists>a\<in>A. \<exists>b\<in>A. (b, a) \<in> r i")
     case True
     then obtain i b c where ibc: "i \<in> I" "b \<in> A" "c \<in> A" "(c,b) \<in> r i"
@@ -344,7 +344,7 @@
 
 lemma wfP_SUP:
   "\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (Domainp (r i)) (Rangep (r j)) = bot \<Longrightarrow>
-    wfP (SUPREMUM UNIV r)"
+    wfP (\<Squnion>(range r))"
   by (rule wf_UN[to_pred]) simp_all
 
 lemma wf_Union: