# HG changeset patch
# User haftmann
# Date 1541664712 -3600
# Node ID 0a9688695a1b83b53a98b6e60445f66923d0c4cd
# Parent  438e1a11445f4f0be3180ecc47915eb18a966504
removed relics of ASCII syntax for indexed big operators

diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Analysis/Binary_Product_Measure.thy
--- a/src/HOL/Analysis/Binary_Product_Measure.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Binary_Product_Measure.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -613,7 +613,7 @@
   have [simp]: "snd \<in> X \<times> Y \<rightarrow> Y" "fst \<in> X \<times> Y \<rightarrow> X"
     by auto
   let ?XY = "{{fst -` a \<inter> X \<times> Y | a. a \<in> A}, {snd -` b \<inter> X \<times> Y | b. b \<in> B}}"
-  have "sets ?P = sets (SUP xy:?XY. sigma (X \<times> Y) xy)"
+  have "sets ?P = sets (SUP xy\<in>?XY. sigma (X \<times> Y) xy)"
     by (simp add: vimage_algebra_sigma sets_pair_eq_sets_fst_snd A B)
   also have "\<dots> = sets (sigma (X \<times> Y) (\<Union>?XY))"
     by (intro Sup_sigma arg_cong[where f=sets]) auto
@@ -713,7 +713,7 @@
   also have "{sigma ?\<Omega> {fst -` Aa \<inter> ?\<Omega> |Aa. Aa \<in> Ea}, sigma ?\<Omega> {snd -` Aa \<inter> ?\<Omega> |Aa. Aa \<in> Eb}} =
     sigma ?\<Omega> ` {{fst -` Aa \<inter> ?\<Omega> |Aa. Aa \<in> Ea}, {snd -` Aa \<inter> ?\<Omega> |Aa. Aa \<in> Eb}}"
     by auto
-  also have "sets (SUP S:{{fst -` Aa \<inter> ?\<Omega> |Aa. Aa \<in> Ea}, {snd -` Aa \<inter> ?\<Omega> |Aa. Aa \<in> Eb}}. sigma ?\<Omega> S) =
+  also have "sets (SUP S\<in>{{fst -` Aa \<inter> ?\<Omega> |Aa. Aa \<in> Ea}, {snd -` Aa \<inter> ?\<Omega> |Aa. Aa \<in> Eb}}. sigma ?\<Omega> S) =
     sets (sigma ?\<Omega> (\<Union>{{fst -` Aa \<inter> ?\<Omega> |Aa. Aa \<in> Ea}, {snd -` Aa \<inter> ?\<Omega> |Aa. Aa \<in> Eb}}))"
     using Ea(1) Eb(1) by (intro sets_Sup_sigma) auto
   also have "\<dots> \<subseteq> sets (sigma ?\<Omega> ?E)"
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Analysis/Borel_Space.thy
--- a/src/HOL/Analysis/Borel_Space.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Borel_Space.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -811,14 +811,14 @@
   fixes F :: "_ \<Rightarrow> _ \<Rightarrow> _::{complete_linorder, linorder_topology, second_countable_topology}"
   assumes [simp]: "countable I"
   assumes [measurable]: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> borel_measurable M"
-  shows "(\<lambda>x. SUP i:I. F i x) \<in> borel_measurable M"
+  shows "(\<lambda>x. SUP i\<in>I. F i x) \<in> borel_measurable M"
   by%unimportant (rule borel_measurableI_greater) (simp add: less_SUP_iff)
 
 lemma%unimportant borel_measurable_INF[measurable (raw)]:
   fixes F :: "_ \<Rightarrow> _ \<Rightarrow> _::{complete_linorder, linorder_topology, second_countable_topology}"
   assumes [simp]: "countable I"
   assumes [measurable]: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> borel_measurable M"
-  shows "(\<lambda>x. INF i:I. F i x) \<in> borel_measurable M"
+  shows "(\<lambda>x. INF i\<in>I. F i x) \<in> borel_measurable M"
   by (rule borel_measurableI_less) (simp add: INF_less_iff)
 
 lemma%unimportant borel_measurable_cSUP[measurable (raw)]:
@@ -826,7 +826,7 @@
   assumes [simp]: "countable I"
   assumes [measurable]: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> borel_measurable M"
   assumes bdd: "\<And>x. x \<in> space M \<Longrightarrow> bdd_above ((\<lambda>i. F i x) ` I)"
-  shows "(\<lambda>x. SUP i:I. F i x) \<in> borel_measurable M"
+  shows "(\<lambda>x. SUP i\<in>I. F i x) \<in> borel_measurable M"
 proof cases
   assume "I = {}" then show ?thesis
     unfolding \<open>I = {}\<close> image_empty by simp
@@ -837,9 +837,9 @@
     fix y
     have "{x \<in> space M. \<forall>i\<in>I. F i x \<le> y} \<in> sets M"
       by measurable
-    also have "{x \<in> space M. \<forall>i\<in>I. F i x \<le> y} = {x \<in> space M. (SUP i:I. F i x) \<le> y}"
+    also have "{x \<in> space M. \<forall>i\<in>I. F i x \<le> y} = {x \<in> space M. (SUP i\<in>I. F i x) \<le> y}"
       by (simp add: cSUP_le_iff \<open>I \<noteq> {}\<close> bdd cong: conj_cong)
-    finally show "{x \<in> space M. (SUP i:I. F i x) \<le>  y} \<in> sets M"  .
+    finally show "{x \<in> space M. (SUP i\<in>I. F i x) \<le>  y} \<in> sets M"  .
   qed
 qed
 
@@ -848,7 +848,7 @@
   assumes [simp]: "countable I"
   assumes [measurable]: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> borel_measurable M"
   assumes bdd: "\<And>x. x \<in> space M \<Longrightarrow> bdd_below ((\<lambda>i. F i x) ` I)"
-  shows "(\<lambda>x. INF i:I. F i x) \<in> borel_measurable M"
+  shows "(\<lambda>x. INF i\<in>I. F i x) \<in> borel_measurable M"
 proof%unimportant cases
   assume "I = {}" then show ?thesis
     unfolding \<open>I = {}\<close> image_empty by simp
@@ -859,9 +859,9 @@
     fix y
     have "{x \<in> space M. \<forall>i\<in>I. y \<le> F i x} \<in> sets M"
       by measurable
-    also have "{x \<in> space M. \<forall>i\<in>I. y \<le> F i x} = {x \<in> space M. y \<le> (INF i:I. F i x)}"
+    also have "{x \<in> space M. \<forall>i\<in>I. y \<le> F i x} = {x \<in> space M. y \<le> (INF i\<in>I. F i x)}"
       by (simp add: le_cINF_iff \<open>I \<noteq> {}\<close> bdd cong: conj_cong)
-    finally show "{x \<in> space M. y \<le> (INF i:I. F i x)} \<in> sets M"  .
+    finally show "{x \<in> space M. y \<le> (INF i\<in>I. F i x)} \<in> sets M"  .
   qed
 qed
 
@@ -1958,22 +1958,22 @@
   fixes F :: "_ \<Rightarrow> _ \<Rightarrow> real"
   assumes [simp]: "countable I"
   assumes F[measurable]: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> borel_measurable M"
-  shows "(\<lambda>x. INF i:I. F i x) \<in> borel_measurable M"
+  shows "(\<lambda>x. INF i\<in>I. F i x) \<in> borel_measurable M"
 proof%unimportant (rule measurable_piecewise_restrict)
   let ?\<Omega> = "{x\<in>space M. bdd_below ((\<lambda>i. F i x)`I)}"
   show "countable {?\<Omega>, - ?\<Omega>}" "space M \<subseteq> \<Union>{?\<Omega>, - ?\<Omega>}" "\<And>X. X \<in> {?\<Omega>, - ?\<Omega>} \<Longrightarrow> X \<inter> space M \<in> sets M"
     by auto
-  fix X assume "X \<in> {?\<Omega>, - ?\<Omega>}" then show "(\<lambda>x. INF i:I. F i x) \<in> borel_measurable (restrict_space M X)"
+  fix X assume "X \<in> {?\<Omega>, - ?\<Omega>}" then show "(\<lambda>x. INF i\<in>I. F i x) \<in> borel_measurable (restrict_space M X)"
   proof safe
-    show "(\<lambda>x. INF i:I. F i x) \<in> borel_measurable (restrict_space M ?\<Omega>)"
+    show "(\<lambda>x. INF i\<in>I. F i x) \<in> borel_measurable (restrict_space M ?\<Omega>)"
       by (intro borel_measurable_cINF measurable_restrict_space1 F)
          (auto simp: space_restrict_space)
-    show "(\<lambda>x. INF i:I. F i x) \<in> borel_measurable (restrict_space M (-?\<Omega>))"
+    show "(\<lambda>x. INF i\<in>I. F i x) \<in> borel_measurable (restrict_space M (-?\<Omega>))"
     proof (subst measurable_cong)
       fix x assume "x \<in> space (restrict_space M (-?\<Omega>))"
       then have "\<not> (\<forall>i\<in>I. - F i x \<le> y)" for y
         by (auto simp: space_restrict_space bdd_above_def bdd_above_uminus[symmetric])
-      then show "(INF i:I. F i x) = - (THE x. False)"
+      then show "(INF i\<in>I. F i x) = - (THE x. False)"
         by (auto simp: space_restrict_space Inf_real_def Sup_real_def Least_def simp del: Set.ball_simps(10))
     qed simp
   qed
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Analysis/Bounded_Continuous_Function.thy
--- a/src/HOL/Analysis/Bounded_Continuous_Function.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Bounded_Continuous_Function.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -45,7 +45,7 @@
   is "\<lambda>f g. (SUP x. dist (f x) (g x))" .
 
 definition uniformity_bcontfun :: "('a \<Rightarrow>\<^sub>C 'b \<times> 'a \<Rightarrow>\<^sub>C 'b) filter"
-  where "uniformity_bcontfun = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+  where "uniformity_bcontfun = (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})"
 
 definition open_bcontfun :: "('a \<Rightarrow>\<^sub>C 'b) set \<Rightarrow> bool"
   where "open_bcontfun S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Analysis/Bounded_Linear_Function.thy
--- a/src/HOL/Analysis/Bounded_Linear_Function.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -150,7 +150,7 @@
   where "dist_blinfun a b = norm (a - b)"
 
 definition [code del]:
-  "(uniformity :: (('a \<Rightarrow>\<^sub>L 'b) \<times> ('a \<Rightarrow>\<^sub>L 'b)) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+  "(uniformity :: (('a \<Rightarrow>\<^sub>L 'b) \<times> ('a \<Rightarrow>\<^sub>L 'b)) filter) = (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})"
 
 definition open_blinfun :: "('a \<Rightarrow>\<^sub>L 'b) set \<Rightarrow> bool"
   where [code del]: "open_blinfun S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Analysis/Caratheodory.thy
--- a/src/HOL/Analysis/Caratheodory.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Caratheodory.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -22,7 +22,7 @@
     using assms by (simp add: fun_eq_iff)
   have reindex: "\<And>B. (\<Sum>x\<in>B. f (prod_decode x)) = sum f (prod_decode ` B)"
     by (simp add: sum.reindex[OF inj_prod_decode] comp_def)
-  have "(SUP n. \<Sum>i<n. f (prod_decode i)) = (SUP p : UNIV \<times> UNIV. \<Sum>i<fst p. \<Sum>n<snd p. f (i, n))"
+  have "(SUP n. \<Sum>i<n. f (prod_decode i)) = (SUP p \<in> UNIV \<times> UNIV. \<Sum>i<fst p. \<Sum>n<snd p. f (i, n))"
   proof (intro SUP_eq; clarsimp simp: sum.cartesian_product reindex)
     fix n
     let ?M = "\<lambda>f. Suc (Max (f ` prod_decode ` {..<n}))"
@@ -299,7 +299,7 @@
 
 definition%important outer_measure :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> 'a set \<Rightarrow> ennreal" where
    "outer_measure M f X =
-     (INF A:{A. range A \<subseteq> M \<and> disjoint_family A \<and> X \<subseteq> (\<Union>i. A i)}. \<Sum>i. f (A i))"
+     (INF A\<in>{A. range A \<subseteq> M \<and> disjoint_family A \<and> X \<subseteq> (\<Union>i. A i)}. \<Sum>i. f (A i))"
 
 lemma%unimportant (in ring_of_sets) outer_measure_agrees:
   assumes posf: "positive M f" and ca: "countably_additive M f" and s: "s \<in> M"
@@ -321,7 +321,7 @@
 next
   have "(\<Sum>i. f (if i = 0 then s else {})) \<le> f s"
     using positiveD1[OF posf] by (subst suminf_finite[of "{0}"]) auto
-  with s show "(INF A:{A. range A \<subseteq> M \<and> disjoint_family A \<and> s \<subseteq> UNION UNIV A}. \<Sum>i. f (A i)) \<le> f s"
+  with s show "(INF A\<in>{A. range A \<subseteq> M \<and> disjoint_family A \<and> s \<subseteq> UNION UNIV A}. \<Sum>i. f (A i)) \<le> f s"
     by (intro INF_lower2[of "\<lambda>i. if i = 0 then s else {}"])
        (auto simp: disjoint_family_on_def)
 qed
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Analysis/Complete_Measure.thy
--- a/src/HOL/Analysis/Complete_Measure.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Complete_Measure.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -452,7 +452,7 @@
 locale cld_measure = complete_measure M + locally_determined_measure M for M :: "'a measure"
 
 definition outer_measure_of :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ennreal"
-  where "outer_measure_of M A = (INF B : {B\<in>sets M. A \<subseteq> B}. emeasure M B)"
+  where "outer_measure_of M A = (INF B \<in> {B\<in>sets M. A \<subseteq> B}. emeasure M B)"
 
 lemma outer_measure_of_eq[simp]: "A \<in> sets M \<Longrightarrow> outer_measure_of M A = emeasure M A"
   by (auto simp: outer_measure_of_def intro!: INF_eqI emeasure_mono)
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Analysis/Connected.thy
--- a/src/HOL/Analysis/Connected.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Connected.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -1057,14 +1057,14 @@
   proof
     assume L: ?lhs
     then have "is_interval S" "compact S" by auto
-    define a where "a \<equiv> \<Sum>i\<in>Basis. (INF x:S. x \<bullet> i) *\<^sub>R i"
-    define b where "b \<equiv> \<Sum>i\<in>Basis. (SUP x:S. x \<bullet> i) *\<^sub>R i"
-    have 1: "\<And>x i. \<lbrakk>x \<in> S; i \<in> Basis\<rbrakk> \<Longrightarrow> (INF x:S. x \<bullet> i) \<le> x \<bullet> i"
+    define a where "a \<equiv> \<Sum>i\<in>Basis. (INF x\<in>S. x \<bullet> i) *\<^sub>R i"
+    define b where "b \<equiv> \<Sum>i\<in>Basis. (SUP x\<in>S. x \<bullet> i) *\<^sub>R i"
+    have 1: "\<And>x i. \<lbrakk>x \<in> S; i \<in> Basis\<rbrakk> \<Longrightarrow> (INF x\<in>S. x \<bullet> i) \<le> x \<bullet> i"
       by (simp add: cInf_lower bounded_inner_imp_bdd_below compact_imp_bounded L)
-    have 2: "\<And>x i. \<lbrakk>x \<in> S; i \<in> Basis\<rbrakk> \<Longrightarrow> x \<bullet> i \<le> (SUP x:S. x \<bullet> i)"
+    have 2: "\<And>x i. \<lbrakk>x \<in> S; i \<in> Basis\<rbrakk> \<Longrightarrow> x \<bullet> i \<le> (SUP x\<in>S. x \<bullet> i)"
       by (simp add: cSup_upper bounded_inner_imp_bdd_above compact_imp_bounded L)
-    have 3: "x \<in> S" if inf: "\<And>i. i \<in> Basis \<Longrightarrow> (INF x:S. x \<bullet> i) \<le> x \<bullet> i"
-                   and sup: "\<And>i. i \<in> Basis \<Longrightarrow> x \<bullet> i \<le> (SUP x:S. x \<bullet> i)" for x
+    have 3: "x \<in> S" if inf: "\<And>i. i \<in> Basis \<Longrightarrow> (INF x\<in>S. x \<bullet> i) \<le> x \<bullet> i"
+                   and sup: "\<And>i. i \<in> Basis \<Longrightarrow> x \<bullet> i \<le> (SUP x\<in>S. x \<bullet> i)" for x
     proof (rule mem_box_componentwiseI [OF \<open>is_interval S\<close>])
       fix i::'a
       assume i: "i \<in> Basis"
@@ -1074,14 +1074,14 @@
         using continuous_attains_inf [OF \<open>compact S\<close> False cont] by blast
       obtain b where "b \<in> S" and b: "\<And>y. y\<in>S \<Longrightarrow> y \<bullet> i \<le> b \<bullet> i"
         using continuous_attains_sup [OF \<open>compact S\<close> False cont] by blast
-      have "a \<bullet> i \<le> (INF x:S. x \<bullet> i)"
+      have "a \<bullet> i \<le> (INF x\<in>S. x \<bullet> i)"
         by (simp add: False a cINF_greatest)
       also have "\<dots> \<le> x \<bullet> i"
         by (simp add: i inf)
       finally have ai: "a \<bullet> i \<le> x \<bullet> i" .
-      have "x \<bullet> i \<le> (SUP x:S. x \<bullet> i)"
+      have "x \<bullet> i \<le> (SUP x\<in>S. x \<bullet> i)"
         by (simp add: i sup)
-      also have "(SUP x:S. x \<bullet> i) \<le> b \<bullet> i"
+      also have "(SUP x\<in>S. x \<bullet> i) \<le> b \<bullet> i"
         by (simp add: False b cSUP_least)
       finally have bi: "x \<bullet> i \<le> b \<bullet> i" .
       show "x \<bullet> i \<in> (\<lambda>x. x \<bullet> i) ` S"
@@ -1282,12 +1282,12 @@
 
 subsection \<open>Infimum Distance\<close>
 
-definition%important "infdist x A = (if A = {} then 0 else INF a:A. dist x a)"
+definition%important "infdist x A = (if A = {} then 0 else INF a\<in>A. dist x a)"
 
 lemma bdd_below_image_dist[intro, simp]: "bdd_below (dist x ` A)"
   by (auto intro!: zero_le_dist)
 
-lemma infdist_notempty: "A \<noteq> {} \<Longrightarrow> infdist x A = (INF a:A. dist x a)"
+lemma infdist_notempty: "A \<noteq> {} \<Longrightarrow> infdist x A = (INF a\<in>A. dist x a)"
   by (simp add: infdist_def)
 
 lemma infdist_nonneg: "0 \<le> infdist x A"
@@ -2665,7 +2665,7 @@
 subsection \<open>The diameter of a set\<close>
 
 definition%important diameter :: "'a::metric_space set \<Rightarrow> real" where
-  "diameter S = (if S = {} then 0 else SUP (x,y):S\<times>S. dist x y)"
+  "diameter S = (if S = {} then 0 else SUP (x,y)\<in>S\<times>S. dist x y)"
 
 lemma diameter_empty [simp]: "diameter{} = 0"
   by (auto simp: diameter_def)
@@ -2696,7 +2696,7 @@
       by (simp add: dist_commute)
   qed
   moreover have "(x,y) \<in> s\<times>s" using s by auto
-  ultimately have "dist x y \<le> (SUP (x,y):s\<times>s. dist x y)"
+  ultimately have "dist x y \<le> (SUP (x,y)\<in>s\<times>s. dist x y)"
     by (rule cSUP_upper2) simp
   with \<open>x \<in> s\<close> show ?thesis
     by (auto simp: diameter_def)
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -5474,7 +5474,7 @@
     apply (erule_tac x="x - y" in ballE)
     apply (auto simp: inner_diff)
     done
-  define k where "k = (SUP x:T. a \<bullet> x)"
+  define k where "k = (SUP x\<in>T. a \<bullet> x)"
   show ?thesis
     apply (rule_tac x="-a" in exI)
     apply (rule_tac x="-(k + b / 2)" in exI)
@@ -5580,7 +5580,7 @@
     using \<open>T \<noteq> {}\<close> by (auto intro: bdd_aboveI2[OF *])
   show ?thesis
     using \<open>a\<noteq>0\<close>
-    by (intro exI[of _ a] exI[of _ "SUP x:S. a \<bullet> x"])
+    by (intro exI[of _ a] exI[of _ "SUP x\<in>S. a \<bullet> x"])
        (auto intro!: cSUP_upper bdd cSUP_least \<open>a \<noteq> 0\<close> \<open>S \<noteq> {}\<close> *)
 qed
 
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Analysis/Embed_Measure.thy
--- a/src/HOL/Analysis/Embed_Measure.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Embed_Measure.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -381,24 +381,24 @@
   assumes nonempty: "Y \<noteq> {}"
   and chain: "Complete_Partial_Order.chain (\<le>) (f ` Y)"
   and countable: "countable B"
-  shows "(\<integral>\<^sup>+ x. (SUP i:Y. f i x) \<partial>count_space B) = (SUP i:Y. (\<integral>\<^sup>+ x. f i x \<partial>count_space B))"
+  shows "(\<integral>\<^sup>+ x. (SUP i\<in>Y. f i x) \<partial>count_space B) = (SUP i\<in>Y. (\<integral>\<^sup>+ x. f i x \<partial>count_space B))"
   (is "?lhs = ?rhs")
 proof -
   let ?f = "(\<lambda>i x. f i (from_nat_into B x) * indicator (to_nat_on B ` B) x)"
-  have "?lhs = \<integral>\<^sup>+ x. (SUP i:Y. f i (from_nat_into B (to_nat_on B x))) \<partial>count_space B"
+  have "?lhs = \<integral>\<^sup>+ x. (SUP i\<in>Y. f i (from_nat_into B (to_nat_on B x))) \<partial>count_space B"
     by(rule nn_integral_cong)(simp add: countable)
-  also have "\<dots> = \<integral>\<^sup>+ x. (SUP i:Y. f i (from_nat_into B x)) \<partial>count_space (to_nat_on B ` B)"
+  also have "\<dots> = \<integral>\<^sup>+ x. (SUP i\<in>Y. f i (from_nat_into B x)) \<partial>count_space (to_nat_on B ` B)"
     by(simp add: embed_measure_count_space'[symmetric] inj_on_to_nat_on countable nn_integral_embed_measure' measurable_embed_measure1)
-  also have "\<dots> = \<integral>\<^sup>+ x. (SUP i:Y. ?f i x) \<partial>count_space UNIV"
+  also have "\<dots> = \<integral>\<^sup>+ x. (SUP i\<in>Y. ?f i x) \<partial>count_space UNIV"
     by(simp add: nn_integral_count_space_indicator ennreal_indicator[symmetric] SUP_mult_right_ennreal nonempty)
-  also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. ?f i x \<partial>count_space UNIV)"
+  also have "\<dots> = (SUP i\<in>Y. \<integral>\<^sup>+ x. ?f i x \<partial>count_space UNIV)"
   proof(rule nn_integral_monotone_convergence_SUP_nat)
     show "Complete_Partial_Order.chain (\<le>) (?f ` Y)"
       by(rule chain_imageI[OF chain, unfolded image_image])(auto intro!: le_funI split: split_indicator dest: le_funD)
   qed fact
-  also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. f i (from_nat_into B x) \<partial>count_space (to_nat_on B ` B))"
+  also have "\<dots> = (SUP i\<in>Y. \<integral>\<^sup>+ x. f i (from_nat_into B x) \<partial>count_space (to_nat_on B ` B))"
     by(simp add: nn_integral_count_space_indicator)
-  also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. f i (from_nat_into B (to_nat_on B x)) \<partial>count_space B)"
+  also have "\<dots> = (SUP i\<in>Y. \<integral>\<^sup>+ x. f i (from_nat_into B (to_nat_on B x)) \<partial>count_space B)"
     by(simp add: embed_measure_count_space'[symmetric] inj_on_to_nat_on countable nn_integral_embed_measure' measurable_embed_measure1)
   also have "\<dots> = ?rhs"
     by(intro arg_cong2[where f="SUPREMUM"] ext nn_integral_cong_AE)(simp_all add: AE_count_space countable)
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -2150,7 +2150,7 @@
   have D_2: "bdd_above (?f`?D)"
     by (metis * mem_Collect_eq bdd_aboveI2)
   note D = D_1 D_2
-  let ?S = "SUP x:?D. ?f x"
+  let ?S = "SUP x\<in>?D. ?f x"
   have *: "\<exists>\<gamma>. gauge \<gamma> \<and>
              (\<forall>p. p tagged_division_of cbox a b \<and>
                   \<gamma> fine p \<longrightarrow>
@@ -2533,7 +2533,7 @@
   have D_2: "bdd_above (?f`?D)"
     by (intro bdd_aboveI2[where M=B] assms(2)[rule_format]) simp
   note D = D_1 D_2
-  let ?S = "SUP d:?D. ?f d"
+  let ?S = "SUP d\<in>?D. ?f d"
   have "\<And>a b. f integrable_on cbox a b"
     using assms(1) integrable_on_subcbox by blast
   then have f_int: "\<And>a b. f absolutely_integrable_on cbox a b"
@@ -3807,7 +3807,7 @@
     by (intro tendsto_lowerbound[OF lim])
        (auto simp: eventually_at_top_linorder)
 
-  have "(SUP i::nat. ?f i x) = ?fR x" for x
+  have "(SUP i. ?f i x) = ?fR x" for x
   proof (rule LIMSEQ_unique[OF LIMSEQ_SUP])
     obtain n where "x - a < real n"
       using reals_Archimedean2[of "x - a"] ..
@@ -3816,16 +3816,16 @@
     then show "(\<lambda>n. ?f n x) \<longlonglongrightarrow> ?fR x"
       by (rule Lim_eventually)
   qed (auto simp: nonneg incseq_def le_fun_def split: split_indicator)
-  then have "integral\<^sup>N lborel ?fR = (\<integral>\<^sup>+ x. (SUP i::nat. ?f i x) \<partial>lborel)"
+  then have "integral\<^sup>N lborel ?fR = (\<integral>\<^sup>+ x. (SUP i. ?f i x) \<partial>lborel)"
     by simp
-  also have "\<dots> = (SUP i::nat. (\<integral>\<^sup>+ x. ?f i x \<partial>lborel))"
+  also have "\<dots> = (SUP i. (\<integral>\<^sup>+ x. ?f i x \<partial>lborel))"
   proof (rule nn_integral_monotone_convergence_SUP)
     show "incseq ?f"
       using nonneg by (auto simp: incseq_def le_fun_def split: split_indicator)
     show "\<And>i. (?f i) \<in> borel_measurable lborel"
       using f_borel by auto
   qed
-  also have "\<dots> = (SUP i::nat. ennreal (F (a + real i) - F a))"
+  also have "\<dots> = (SUP i. ennreal (F (a + real i) - F a))"
     by (subst nn_integral_FTC_Icc[OF f_borel f nonneg]) auto
   also have "\<dots> = T - F a"
   proof (rule LIMSEQ_unique[OF LIMSEQ_SUP])
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Analysis/Extended_Real_Limits.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Extended_Real_Limits.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -298,7 +298,7 @@
 
 lemma%important Liminf_within:
   fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
-  shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S \<inter> ball x e - {x}). f y)"
+  shows "Liminf (at x within S) f = (SUP e\<in>{0<..}. INF y\<in>(S \<inter> ball x e - {x}). f y)"
   unfolding Liminf_def eventually_at
 proof%unimportant (rule SUP_eq, simp_all add: Ball_def Bex_def, safe)
   fix P d
@@ -318,7 +318,7 @@
 
 lemma%important Limsup_within:
   fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
-  shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S \<inter> ball x e - {x}). f y)"
+  shows "Limsup (at x within S) f = (INF e\<in>{0<..}. SUP y\<in>(S \<inter> ball x e - {x}). f y)"
   unfolding Limsup_def eventually_at
 proof%unimportant (rule INF_eq, simp_all add: Ball_def Bex_def, safe)
   fix P d
@@ -338,17 +338,17 @@
 
 lemma Liminf_at:
   fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
-  shows "Liminf (at x) f = (SUP e:{0<..}. INF y:(ball x e - {x}). f y)"
+  shows "Liminf (at x) f = (SUP e\<in>{0<..}. INF y\<in>(ball x e - {x}). f y)"
   using Liminf_within[of x UNIV f] by simp
 
 lemma Limsup_at:
   fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
-  shows "Limsup (at x) f = (INF e:{0<..}. SUP y:(ball x e - {x}). f y)"
+  shows "Limsup (at x) f = (INF e\<in>{0<..}. SUP y\<in>(ball x e - {x}). f y)"
   using Limsup_within[of x UNIV f] by simp
 
 lemma min_Liminf_at:
   fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_linorder"
-  shows "min (f x) (Liminf (at x) f) = (SUP e:{0<..}. INF y:ball x e. f y)"
+  shows "min (f x) (Liminf (at x) f) = (SUP e\<in>{0<..}. INF y\<in>ball x e. f y)"
   unfolding inf_min[symmetric] Liminf_at
   apply (subst inf_commute)
   apply (subst SUP_inf)
@@ -1231,16 +1231,16 @@
 lemma limsup_shift:
   "limsup (\<lambda>n. u (n+1)) = limsup u"
 proof -
-  have "(SUP m:{n+1..}. u m) = (SUP m:{n..}. u (m + 1))" for n
+  have "(SUP m\<in>{n+1..}. u m) = (SUP m\<in>{n..}. u (m + 1))" for n
     apply (rule SUP_eq) using Suc_le_D by auto
-  then have a: "(INF n. SUP m:{n..}. u (m + 1)) = (INF n. (SUP m:{n+1..}. u m))" by auto
-  have b: "(INF n. (SUP m:{n+1..}. u m)) = (INF n:{1..}. (SUP m:{n..}. u m))"
+  then have a: "(INF n. SUP m\<in>{n..}. u (m + 1)) = (INF n. (SUP m\<in>{n+1..}. u m))" by auto
+  have b: "(INF n. (SUP m\<in>{n+1..}. u m)) = (INF n\<in>{1..}. (SUP m\<in>{n..}. u m))"
     apply (rule INF_eq) using Suc_le_D by auto
-  have "(INF n:{1..}. v n) = (INF n. v n)" if "decseq v" for v::"nat \<Rightarrow> 'a"
+  have "(INF n\<in>{1..}. v n) = (INF n. v n)" if "decseq v" for v::"nat \<Rightarrow> 'a"
     apply (rule INF_eq) using \<open>decseq v\<close> decseq_Suc_iff by auto
-  moreover have "decseq (\<lambda>n. (SUP m:{n..}. u m))" by (simp add: SUP_subset_mono decseq_def)
-  ultimately have c: "(INF n:{1..}. (SUP m:{n..}. u m)) = (INF n. (SUP m:{n..}. u m))" by simp
-  have "(INF n. SUPREMUM {n..} u) = (INF n. SUP m:{n..}. u (m + 1))" using a b c by simp
+  moreover have "decseq (\<lambda>n. (SUP m\<in>{n..}. u m))" by (simp add: SUP_subset_mono decseq_def)
+  ultimately have c: "(INF n\<in>{1..}. (SUP m\<in>{n..}. u m)) = (INF n. (SUP m\<in>{n..}. u m))" by simp
+  have "(INF n. SUPREMUM {n..} u) = (INF n. SUP m\<in>{n..}. u (m + 1))" using a b c by simp
   then show ?thesis by (auto cong: limsup_INF_SUP)
 qed
 
@@ -1255,16 +1255,16 @@
 lemma liminf_shift:
   "liminf (\<lambda>n. u (n+1)) = liminf u"
 proof -
-  have "(INF m:{n+1..}. u m) = (INF m:{n..}. u (m + 1))" for n
+  have "(INF m\<in>{n+1..}. u m) = (INF m\<in>{n..}. u (m + 1))" for n
     apply (rule INF_eq) using Suc_le_D by (auto)
-  then have a: "(SUP n. INF m:{n..}. u (m + 1)) = (SUP n. (INF m:{n+1..}. u m))" by auto
-  have b: "(SUP n. (INF m:{n+1..}. u m)) = (SUP n:{1..}. (INF m:{n..}. u m))"
+  then have a: "(SUP n. INF m\<in>{n..}. u (m + 1)) = (SUP n. (INF m\<in>{n+1..}. u m))" by auto
+  have b: "(SUP n. (INF m\<in>{n+1..}. u m)) = (SUP n\<in>{1..}. (INF m\<in>{n..}. u m))"
     apply (rule SUP_eq) using Suc_le_D by (auto)
-  have "(SUP n:{1..}. v n) = (SUP n. v n)" if "incseq v" for v::"nat \<Rightarrow> 'a"
+  have "(SUP n\<in>{1..}. v n) = (SUP n. v n)" if "incseq v" for v::"nat \<Rightarrow> 'a"
     apply (rule SUP_eq) using \<open>incseq v\<close> incseq_Suc_iff by auto
-  moreover have "incseq (\<lambda>n. (INF m:{n..}. u m))" by (simp add: INF_superset_mono mono_def)
-  ultimately have c: "(SUP n:{1..}. (INF m:{n..}. u m)) = (SUP n. (INF m:{n..}. u m))" by simp
-  have "(SUP n. INFIMUM {n..} u) = (SUP n. INF m:{n..}. u (m + 1))" using a b c by simp
+  moreover have "incseq (\<lambda>n. (INF m\<in>{n..}. u m))" by (simp add: INF_superset_mono mono_def)
+  ultimately have c: "(SUP n\<in>{1..}. (INF m\<in>{n..}. u m)) = (SUP n. (INF m\<in>{n..}. u m))" by simp
+  have "(SUP n. INFIMUM {n..} u) = (SUP n. INF m\<in>{n..}. u (m + 1))" using a b c by simp
   then show ?thesis by (auto cong: liminf_SUP_INF)
 qed
 
@@ -1281,7 +1281,7 @@
   assumes "Limsup F u > c"
   shows "\<exists>i. u i > c"
 proof%unimportant -
-  have "(INF P:{P. eventually P F}. SUP x:{x. P x}. u x) > c" using assms by (simp add: Limsup_def)
+  have "(INF P\<in>{P. eventually P F}. SUP x\<in>{x. P x}. u x) > c" using assms by (simp add: Limsup_def)
   then show ?thesis by (metis eventually_True mem_Collect_eq less_INF_D less_SUP_iff)
 qed
 
@@ -1297,7 +1297,7 @@
     by (intro dependent_nat_choice) (auto simp: conj_commute)
   then obtain r :: "nat \<Rightarrow> nat" where "strict_mono r" and mono: "\<And>n m. r n \<le> m \<Longrightarrow> u m \<le> u (r n)"
     by (auto simp: strict_mono_Suc_iff)
-  define umax where "umax = (\<lambda>n. (SUP m:{n..}. u m))"
+  define umax where "umax = (\<lambda>n. (SUP m\<in>{n..}. u m))"
   have "decseq umax" unfolding umax_def by (simp add: SUP_subset_mono antimono_def)
   then have "umax \<longlonglongrightarrow> limsup u" unfolding umax_def by (metis LIMSEQ_INF limsup_INF_SUP)
   then have *: "(umax o r) \<longlonglongrightarrow> limsup u" by (simp add: LIMSEQ_subseq_LIMSEQ \<open>strict_mono r\<close>)
@@ -1373,7 +1373,7 @@
     then have "u i \<le> u (r(Suc n))" using r by simp
     then have "u i \<le> (SUP n. (u o r) n)" unfolding o_def by (meson SUP_upper2 UNIV_I)
   }
-  then have "(SUP i:{N<..}. u i) \<le> (SUP n. (u o r) n)" using SUP_least by blast
+  then have "(SUP i\<in>{N<..}. u i) \<le> (SUP n. (u o r) n)" using SUP_least by blast
   then have "limsup u \<le> (SUP n. (u o r) n)" unfolding Limsup_def
     by (metis (mono_tags, lifting) INF_lower2 atLeast_Suc_greaterThan atLeast_def eventually_ge_at_top mem_Collect_eq)
   then have "limsup u = (SUP n. (u o r) n)" using \<open>(SUP n. (u o r) n) \<le> limsup u\<close> by simp
@@ -1390,7 +1390,7 @@
     by (intro dependent_nat_choice) (auto simp: conj_commute)
   then obtain r :: "nat \<Rightarrow> nat" where "strict_mono r" and mono: "\<And>n m. r n \<le> m \<Longrightarrow> u m \<ge> u (r n)"
     by (auto simp: strict_mono_Suc_iff)
-  define umin where "umin = (\<lambda>n. (INF m:{n..}. u m))"
+  define umin where "umin = (\<lambda>n. (INF m\<in>{n..}. u m))"
   have "incseq umin" unfolding umin_def by (simp add: INF_superset_mono incseq_def)
   then have "umin \<longlonglongrightarrow> liminf u" unfolding umin_def by (metis LIMSEQ_SUP liminf_SUP_INF)
   then have *: "(umin o r) \<longlonglongrightarrow> liminf u" by (simp add: LIMSEQ_subseq_LIMSEQ \<open>strict_mono r\<close>)
@@ -1467,7 +1467,7 @@
     then have "u i \<ge> u (r(Suc n))" using r by simp
     then have "u i \<ge> (INF n. (u o r) n)" unfolding o_def by (meson INF_lower2 UNIV_I)
   }
-  then have "(INF i:{N<..}. u i) \<ge> (INF n. (u o r) n)" using INF_greatest by blast
+  then have "(INF i\<in>{N<..}. u i) \<ge> (INF n. (u o r) n)" using INF_greatest by blast
   then have "liminf u \<ge> (INF n. (u o r) n)" unfolding Liminf_def
     by (metis (mono_tags, lifting) SUP_upper2 atLeast_Suc_greaterThan atLeast_def eventually_ge_at_top mem_Collect_eq)
   then have "liminf u = (INF n. (u o r) n)" using \<open>(INF n. (u o r) n) \<ge> liminf u\<close> by simp
@@ -1757,7 +1757,7 @@
     using * by (intro SUP_upper2[of x]) auto
   moreover have "0 \<le> (SUPREMUM {x..} u)" for x
     using * by (intro SUP_upper2[of x]) auto
-  ultimately show "(SUP n. INF n:{n..}. max 0 (u n - v n))
+  ultimately show "(SUP n. INF n\<in>{n..}. max 0 (u n - v n))
             \<le> max 0 ((INF x. max 0 (SUPREMUM {x..} u)) - (INF x. max 0 (SUPREMUM {x..} v)))"
     by (auto simp: * ereal_diff_positive max.absorb2 liminf_SUP_INF[symmetric] limsup_INF_SUP[symmetric] ereal_liminf_limsup_minus)
 qed
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -459,7 +459,7 @@
 
 definition%important [code del]:
   "(uniformity :: (('a^'b::_) \<times> ('a^'b::_)) filter) =
-    (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+    (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})"
 
 instance%unimportant
   by standard (rule uniformity_vec_def)
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Analysis/Finite_Product_Measure.thy
--- a/src/HOL/Analysis/Finite_Product_Measure.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -389,7 +389,7 @@
 qed
 
 lemma%unimportant sets_PiM_eq_proj:
-  "I \<noteq> {} \<Longrightarrow> sets (PiM I M) = sets (SUP i:I. vimage_algebra (\<Pi>\<^sub>E i\<in>I. space (M i)) (\<lambda>x. x i) (M i))"
+  "I \<noteq> {} \<Longrightarrow> sets (PiM I M) = sets (SUP i\<in>I. vimage_algebra (\<Pi>\<^sub>E i\<in>I. space (M i)) (\<lambda>x. x i) (M i))"
   apply (simp add: sets_PiM_single)
   apply (subst sets_Sup_eq[where X="\<Pi>\<^sub>E i\<in>I. space (M i)"])
   apply auto []
@@ -422,9 +422,9 @@
   let ?F = "\<lambda>i. {(\<lambda>x. x i) -` A \<inter> Pi\<^sub>E I \<Omega> |A. A \<in> E i}"
   assume "I \<noteq> {}"
   then have "sets (Pi\<^sub>M I (\<lambda>i. sigma (\<Omega> i) (E i))) =
-      sets (SUP i:I. vimage_algebra (\<Pi>\<^sub>E i\<in>I. \<Omega> i) (\<lambda>x. x i) (sigma (\<Omega> i) (E i)))"
+      sets (SUP i\<in>I. vimage_algebra (\<Pi>\<^sub>E i\<in>I. \<Omega> i) (\<lambda>x. x i) (sigma (\<Omega> i) (E i)))"
     by (subst sets_PiM_eq_proj) (auto simp: space_measure_of_conv)
-  also have "\<dots> = sets (SUP i:I. sigma (Pi\<^sub>E I \<Omega>) (?F i))"
+  also have "\<dots> = sets (SUP i\<in>I. sigma (Pi\<^sub>E I \<Omega>) (?F i))"
     using E by (intro sets_SUP_cong arg_cong[where f=sets] vimage_algebra_sigma) auto
   also have "\<dots> = sets (sigma (Pi\<^sub>E I \<Omega>) (\<Union>i\<in>I. ?F i))"
     using \<open>I \<noteq> {}\<close> by (intro arg_cong[where f=sets] SUP_sigma_sigma) auto
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Analysis/Function_Topology.thy
--- a/src/HOL/Analysis/Function_Topology.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Function_Topology.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -1220,7 +1220,7 @@
   "dist x y = (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
 
 definition%important uniformity_fun_def:
-  "(uniformity::(('a \<Rightarrow> 'b) \<times> ('a \<Rightarrow> 'b)) filter) = (INF e:{0<..}. principal {(x, y). dist (x::('a\<Rightarrow>'b)) y < e})"
+  "(uniformity::(('a \<Rightarrow> 'b) \<times> ('a \<Rightarrow> 'b)) filter) = (INF e\<in>{0<..}. principal {(x, y). dist (x::('a\<Rightarrow>'b)) y < e})"
 
 text \<open>Except for the first one, the auxiliary lemmas below are only useful when proving the
 instance: once it is proved, they become trivial consequences of the general theory of metric
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Analysis/Gamma_Function.thy
--- a/src/HOL/Analysis/Gamma_Function.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Gamma_Function.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -372,7 +372,7 @@
   shows "uniformly_convergent_on (ball z d) (\<lambda>n z. ln_Gamma_series z n :: complex)"
 proof (intro Cauchy_uniformly_convergent uniformly_Cauchy_onI')
   fix e :: real assume e: "e > 0"
-  define e'' where "e'' = (SUP t:ball z d. norm t + norm t^2)"
+  define e'' where "e'' = (SUP t\<in>ball z d. norm t + norm t^2)"
   define e' where "e' = e / (2*e'')"
   have "bounded ((\<lambda>t. norm t + norm t^2) ` cball z d)"
     by (intro compact_imp_bounded compact_continuous_image) (auto intro!: continuous_intros)
@@ -2270,7 +2270,7 @@
     qed
     ultimately have compact: "compact B" by (subst compact_eq_bounded_closed) blast
 
-    define M where "M = (SUP z:B. norm (h' z))"
+    define M where "M = (SUP z\<in>B. norm (h' z))"
     have "compact (h' ` B)"
       by (intro compact_continuous_image continuous_on_subset[OF h'_cont] compact) blast+
     hence bdd: "bdd_above ((\<lambda>z. norm (h' z)) ` B)"
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Analysis/Improper_Integral.thy
--- a/src/HOL/Analysis/Improper_Integral.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Improper_Integral.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -674,9 +674,9 @@
     qed
   qed
   define \<gamma> where "\<gamma> \<equiv> \<lambda>x. \<gamma>0 x \<inter>
-                          ball x ((\<epsilon>/8 / (norm(f x) + 1)) * (INF m:Basis. b \<bullet> m - a \<bullet> m) / content(cbox a b))"
+                          ball x ((\<epsilon>/8 / (norm(f x) + 1)) * (INF m\<in>Basis. b \<bullet> m - a \<bullet> m) / content(cbox a b))"
   have "gauge (\<lambda>x. ball x
-                    (\<epsilon> * (INF m:Basis. b \<bullet> m - a \<bullet> m) / ((8 * norm (f x) + 8) * content (cbox a b))))"
+                    (\<epsilon> * (INF m\<in>Basis. b \<bullet> m - a \<bullet> m) / ((8 * norm (f x) + 8) * content (cbox a b))))"
     using \<open>0 < content (cbox a b)\<close> \<open>0 < \<epsilon>\<close> a_less_b
     apply (auto simp: gauge_def divide_simps mult_less_0_iff zero_less_mult_iff add_nonneg_eq_0_iff finite_less_Inf_iff)
     apply (meson add_nonneg_nonneg mult_nonneg_nonneg norm_ge_zero not_less zero_le_numeral)
@@ -693,7 +693,7 @@
     have "finite S"
       using S by blast
     have "\<gamma>0 fine S" and fineS:
-         "(\<lambda>x. ball x (\<epsilon> * (INF m:Basis. b \<bullet> m - a \<bullet> m) / ((8 * norm (f x) + 8) * content (cbox a b)))) fine S"
+         "(\<lambda>x. ball x (\<epsilon> * (INF m\<in>Basis. b \<bullet> m - a \<bullet> m) / ((8 * norm (f x) + 8) * content (cbox a b)))) fine S"
       using \<open>\<gamma> fine S\<close> by (auto simp: \<gamma>_def fine_Int)
     then have "(\<Sum>(x,K) \<in> S. norm (content K *\<^sub>R h x - integral K h)) < \<epsilon>/2"
       by (intro \<gamma>0 that fineS)
@@ -735,11 +735,11 @@
             using that by auto
           ultimately have "norm (h x) \<le> (\<epsilon> * (b \<bullet> i - a \<bullet> i)) / (4 * content (cbox a b) * ?\<Delta>)"
           proof -
-            have "dist x u < \<epsilon> * (INF m:Basis. b \<bullet> m - a \<bullet> m) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2"
-                 "dist x v < \<epsilon> * (INF m:Basis. b \<bullet> m - a \<bullet> m) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2"
+            have "dist x u < \<epsilon> * (INF m\<in>Basis. b \<bullet> m - a \<bullet> m) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2"
+                 "dist x v < \<epsilon> * (INF m\<in>Basis. b \<bullet> m - a \<bullet> m) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2"
               using fineS u_less_v uv xK
               by (force simp: fine_def mem_box field_simps dest!: bspec)+
-            moreover have "\<epsilon> * (INF m:Basis. b \<bullet> m - a \<bullet> m) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2
+            moreover have "\<epsilon> * (INF m\<in>Basis. b \<bullet> m - a \<bullet> m) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2
                   \<le> \<epsilon> * (b \<bullet> i - a \<bullet> i) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2"
               apply (intro mult_left_mono divide_right_mono)
               using \<open>i \<in> Basis\<close> \<open>0 < \<epsilon>\<close> apply (auto simp: intro!: cInf_le_finite)
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Analysis/Lebesgue_Measure.thy
--- a/src/HOL/Analysis/Lebesgue_Measure.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -1189,7 +1189,7 @@
       using emeasure_bounded_finite[of "?B n"] by (auto simp: emeasure_A)
     interpret A: finite_measure ?A
       by rule fact
-    have "emeasure ?A B + ?e n > (INF U:{U. B \<subseteq> U \<and> open U}. emeasure ?A U)"
+    have "emeasure ?A B + ?e n > (INF U\<in>{U. B \<subseteq> U \<and> open U}. emeasure ?A U)"
       using \<open>0<e\<close> by (auto simp: outer_regular[OF _ finite_A B, symmetric])
     then obtain U where U: "B \<subseteq> U" "open U" and muU: "?\<mu> (?B n \<inter> B) + ?e n > ?\<mu> (?B n \<inter> U)"
       unfolding INF_less_iff by (auto simp: emeasure_A)
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Analysis/Measurable.thy
--- a/src/HOL/Analysis/Measurable.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Measurable.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -392,32 +392,32 @@
   fixes F :: "'i \<Rightarrow> 'a \<Rightarrow> 'b::{complete_lattice, countable}"
   assumes [simp]: "countable I"
   assumes [measurable]: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> measurable M (count_space UNIV)"
-  shows "(\<lambda>x. SUP i:I. F i x) \<in> measurable M (count_space UNIV)"
+  shows "(\<lambda>x. SUP i\<in>I. F i x) \<in> measurable M (count_space UNIV)"
   unfolding measurable_count_space_eq2_countable
 proof (safe intro!: UNIV_I)
   fix a
-  have "(\<lambda>x. SUP i:I. F i x) -` {a} \<inter> space M =
+  have "(\<lambda>x. SUP i\<in>I. F i x) -` {a} \<inter> space M =
     {x\<in>space M. (\<forall>i\<in>I. F i x \<le> a) \<and> (\<forall>b. (\<forall>i\<in>I. F i x \<le> b) \<longrightarrow> a \<le> b)}"
     unfolding SUP_le_iff[symmetric] by auto
   also have "\<dots> \<in> sets M"
     by measurable
-  finally show "(\<lambda>x. SUP i:I. F i x) -` {a} \<inter> space M \<in> sets M" .
+  finally show "(\<lambda>x. SUP i\<in>I. F i x) -` {a} \<inter> space M \<in> sets M" .
 qed
 
 lemma measurable_INF[measurable]:
   fixes F :: "'i \<Rightarrow> 'a \<Rightarrow> 'b::{complete_lattice, countable}"
   assumes [simp]: "countable I"
   assumes [measurable]: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> measurable M (count_space UNIV)"
-  shows "(\<lambda>x. INF i:I. F i x) \<in> measurable M (count_space UNIV)"
+  shows "(\<lambda>x. INF i\<in>I. F i x) \<in> measurable M (count_space UNIV)"
   unfolding measurable_count_space_eq2_countable
 proof (safe intro!: UNIV_I)
   fix a
-  have "(\<lambda>x. INF i:I. F i x) -` {a} \<inter> space M =
+  have "(\<lambda>x. INF i\<in>I. F i x) -` {a} \<inter> space M =
     {x\<in>space M. (\<forall>i\<in>I. a \<le> F i x) \<and> (\<forall>b. (\<forall>i\<in>I. b \<le> F i x) \<longrightarrow> b \<le> a)}"
     unfolding le_INF_iff[symmetric] by auto
   also have "\<dots> \<in> sets M"
     by measurable
-  finally show "(\<lambda>x. INF i:I. F i x) -` {a} \<inter> space M \<in> sets M" .
+  finally show "(\<lambda>x. INF i\<in>I. F i x) -` {a} \<inter> space M \<in> sets M" .
 qed
 
 lemma measurable_lfp_coinduct[consumes 1, case_names continuity step]:
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -582,12 +582,12 @@
   assumes I: "I \<noteq> {}" and F: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> i \<le> j \<Longrightarrow> F j \<subseteq> F i"
   assumes F_sets[measurable]: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> sets M"
     and fin: "\<And>i. i \<in> I \<Longrightarrow> emeasure M (F i) \<noteq> \<infinity>"
-  shows "emeasure M (\<Inter>i\<in>I. F i) = (INF i:I. emeasure M (F i))"
+  shows "emeasure M (\<Inter>i\<in>I. F i) = (INF i\<in>I. emeasure M (F i))"
 proof cases
   assume "finite I"
   have "(\<Inter>i\<in>I. F i) = F (Max I)"
     using I \<open>finite I\<close> by (intro antisym INF_lower INF_greatest F) auto
-  moreover have "(INF i:I. emeasure M (F i)) = emeasure M (F (Max I))"
+  moreover have "(INF i\<in>I. emeasure M (F i)) = emeasure M (F (Max I))"
     using I \<open>finite I\<close> by (intro antisym INF_lower INF_greatest F emeasure_mono) auto
   ultimately show ?thesis
     by simp
@@ -611,7 +611,7 @@
     show "decseq (\<lambda>i. F (L i))"
       using L by (intro antimonoI F L_mono) auto
   qed (insert L fin, auto)
-  also have "\<dots> = (INF i:I. emeasure M (F i))"
+  also have "\<dots> = (INF i\<in>I. emeasure M (F i))"
   proof (intro antisym INF_greatest)
     show "i \<in> I \<Longrightarrow> (INF i. emeasure M (F (L i))) \<le> emeasure M (F i)" for i
       by (intro INF_lower2[of i]) auto
@@ -990,7 +990,7 @@
 subsection \<open>The almost everywhere filter (i.e.\ quantifier)\<close>
 
 definition%important ae_filter :: "'a measure \<Rightarrow> 'a filter" where
-  "ae_filter M = (INF N:null_sets M. principal (space M - N))"
+  "ae_filter M = (INF N\<in>null_sets M. principal (space M - N))"
 
 abbreviation almost_everywhere :: "'a measure \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
   "almost_everywhere M P \<equiv> eventually P (ae_filter M)"
@@ -2702,7 +2702,7 @@
     by (intro bdd_aboveI[where M="measure M (space M)"])
        (auto simp: d_def field_simps subset_eq intro!: add_increasing M.finite_measure_mono)
 
-  define \<gamma> where "\<gamma> = (SUP X:sets M. d X)"
+  define \<gamma> where "\<gamma> = (SUP X\<in>sets M. d X)"
   have le_\<gamma>[intro]: "X \<in> sets M \<Longrightarrow> d X \<le> \<gamma>" for X
     by (auto simp: \<gamma>_def intro!: cSUP_upper)
 
@@ -2876,7 +2876,7 @@
 
 definition%important sup_measure' :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
 where
-  "sup_measure' A B = measure_of (space A) (sets A) (\<lambda>X. SUP Y:sets A. emeasure A (X \<inter> Y) + emeasure B (X \<inter> - Y))"
+  "sup_measure' A B = measure_of (space A) (sets A) (\<lambda>X. SUP Y\<in>sets A. emeasure A (X \<inter> Y) + emeasure B (X \<inter> - Y))"
 
 lemma assumes [simp]: "sets B = sets A"
   shows space_sup_measure'[simp]: "space (sup_measure' A B) = space A"
@@ -2885,7 +2885,7 @@
 
 lemma emeasure_sup_measure':
   assumes sets_eq[simp]: "sets B = sets A" and [simp, intro]: "X \<in> sets A"
-  shows "emeasure (sup_measure' A B) X = (SUP Y:sets A. emeasure A (X \<inter> Y) + emeasure B (X \<inter> - Y))"
+  shows "emeasure (sup_measure' A B) X = (SUP Y\<in>sets A. emeasure A (X \<inter> Y) + emeasure B (X \<inter> - Y))"
     (is "_ = ?S X")
 proof -
   note sets_eq_imp_space_eq[OF sets_eq, simp]
@@ -2893,12 +2893,12 @@
     using sup_measure'_def
   proof (rule emeasure_measure_of)
     let ?d = "\<lambda>X Y. emeasure A (X \<inter> Y) + emeasure B (X \<inter> - Y)"
-    show "countably_additive (sets (sup_measure' A B)) (\<lambda>X. SUP Y : sets A. emeasure A (X \<inter> Y) + emeasure B (X \<inter> - Y))"
+    show "countably_additive (sets (sup_measure' A B)) (\<lambda>X. SUP Y \<in> sets A. emeasure A (X \<inter> Y) + emeasure B (X \<inter> - Y))"
     proof (rule countably_additiveI, goal_cases)
       case (1 X)
       then have [measurable]: "\<And>i. X i \<in> sets A" and "disjoint_family X"
         by auto
-      have "(\<Sum>i. ?S (X i)) = (SUP Y:sets A. \<Sum>i. ?d (X i) Y)"
+      have "(\<Sum>i. ?S (X i)) = (SUP Y\<in>sets A. \<Sum>i. ?d (X i) Y)"
       proof (rule ennreal_suminf_SUP_eq_directed)
         fix J :: "nat set" and a b assume "finite J" and [measurable]: "a \<in> sets A" "b \<in> sets A"
         have "\<exists>c\<in>sets A. c \<subseteq> X i \<and> (\<forall>a\<in>sets A. ?d (X i) a \<le> ?d (X i) c)" for i
@@ -2988,7 +2988,7 @@
   assumes B: "\<And>Y. Y \<subseteq> X \<Longrightarrow> Y \<in> sets A \<Longrightarrow> emeasure B Y \<le> emeasure C Y"
   shows "emeasure (sup_measure' A B) X \<le> emeasure C X"
 proof (subst emeasure_sup_measure')
-  show "(SUP Y:sets A. emeasure A (X \<inter> Y) + emeasure B (X \<inter> - Y)) \<le> emeasure C X"
+  show "(SUP Y\<in>sets A. emeasure A (X \<inter> Y) + emeasure B (X \<inter> - Y)) \<le> emeasure C X"
     unfolding \<open>sets A = sets C\<close>
   proof (intro SUP_least)
     fix Y assume [measurable]: "Y \<in> sets C"
@@ -3137,10 +3137,10 @@
 
 definition Sup_lexord :: "('a \<Rightarrow> 'b::complete_lattice) \<Rightarrow> ('a set \<Rightarrow> 'a) \<Rightarrow> ('a set \<Rightarrow> 'a) \<Rightarrow> 'a set \<Rightarrow> 'a"
 where
-  "Sup_lexord k c s A = (let U = (SUP a:A. k a) in if \<exists>a\<in>A. k a = U then c {a\<in>A. k a = U} else s A)"
+  "Sup_lexord k c s A = (let U = (SUP a\<in>A. k a) in if \<exists>a\<in>A. k a = U then c {a\<in>A. k a = U} else s A)"
 
 lemma Sup_lexord:
-  "(\<And>a S. a \<in> A \<Longrightarrow> k a = (SUP a:A. k a) \<Longrightarrow> S = {a'\<in>A. k a' = k a} \<Longrightarrow> P (c S)) \<Longrightarrow> ((\<And>a. a \<in> A \<Longrightarrow> k a \<noteq> (SUP a:A. k a)) \<Longrightarrow> P (s A)) \<Longrightarrow>
+  "(\<And>a S. a \<in> A \<Longrightarrow> k a = (SUP a\<in>A. k a) \<Longrightarrow> S = {a'\<in>A. k a' = k a} \<Longrightarrow> P (c S)) \<Longrightarrow> ((\<And>a. a \<in> A \<Longrightarrow> k a \<noteq> (SUP a\<in>A. k a)) \<Longrightarrow> P (s A)) \<Longrightarrow>
     P (Sup_lexord k c s A)"
   by (auto simp: Sup_lexord_def Let_def)
 
@@ -3197,7 +3197,7 @@
 definition%important Sup_measure' :: "'a measure set \<Rightarrow> 'a measure"
 where
   "Sup_measure' M = measure_of (\<Union>a\<in>M. space a) (\<Union>a\<in>M. sets a)
-    (\<lambda>X. (SUP P:{P. finite P \<and> P \<subseteq> M }. sup_measure.F id P X))"
+    (\<lambda>X. (SUP P\<in>{P. finite P \<and> P \<subseteq> M }. sup_measure.F id P X))"
 
 lemma space_Sup_measure'2: "space (Sup_measure' M) = (\<Union>m\<in>M. space m)"
   unfolding Sup_measure'_def by (intro space_measure_of[OF UN_space_closed])
@@ -3218,7 +3218,7 @@
 
 lemma emeasure_Sup_measure':
   assumes sets_eq[simp]: "\<And>m. m \<in> M \<Longrightarrow> sets m = sets A" and "X \<in> sets A" "M \<noteq> {}"
-  shows "emeasure (Sup_measure' M) X = (SUP P:{P. finite P \<and> P \<subseteq> M}. sup_measure.F id P X)"
+  shows "emeasure (Sup_measure' M) X = (SUP P\<in>{P. finite P \<and> P \<subseteq> M}. sup_measure.F id P X)"
     (is "_ = ?S X")
   using Sup_measure'_def
 proof (rule emeasure_measure_of)
@@ -3245,7 +3245,7 @@
       with ij show "\<exists>k\<in>{P. finite P \<and> P \<subseteq> M}. \<forall>n\<in>N. ?\<mu> i (F n) \<le> ?\<mu> k (F n) \<and> ?\<mu> j (F n) \<le> ?\<mu> k (F n)"
         by (safe intro!: bexI[of _ "i \<union> j"]) auto
     next
-      show "(SUP P : {P. finite P \<and> P \<subseteq> M}. \<Sum>n. ?\<mu> P (F n)) = (SUP P : {P. finite P \<and> P \<subseteq> M}. ?\<mu> P (UNION UNIV F))"
+      show "(SUP P \<in> {P. finite P \<and> P \<subseteq> M}. \<Sum>n. ?\<mu> P (F n)) = (SUP P \<in> {P. finite P \<and> P \<subseteq> M}. ?\<mu> P (UNION UNIV F))"
       proof (intro SUP_cong refl)
         fix i assume i: "i \<in> {P. finite P \<and> P \<subseteq> M}"
         show "(\<Sum>n. ?\<mu> i (F n)) = ?\<mu> i (UNION UNIV F)"
@@ -3337,7 +3337,7 @@
           fix X assume "X \<in> sets x"
           show "emeasure x X \<le> emeasure (Sup_measure' S') X"
           proof (subst emeasure_Sup_measure'[OF _ \<open>X \<in> sets x\<close>])
-            show "emeasure x X \<le> (SUP P : {P. finite P \<and> P \<subseteq> S'}. emeasure (sup_measure.F id P) X)"
+            show "emeasure x X \<le> (SUP P \<in> {P. finite P \<and> P \<subseteq> S'}. emeasure (sup_measure.F id P) X)"
               using \<open>x\<in>S'\<close> by (intro SUP_upper2[where i="{x}"]) auto
           qed (insert \<open>x\<in>S'\<close> S', auto)
         qed
@@ -3401,7 +3401,7 @@
           show "emeasure (Sup_measure' S') X \<le> emeasure x X"
             unfolding ***
           proof (subst emeasure_Sup_measure'[OF _ \<open>X \<in> sets (Sup_measure' S')\<close>])
-            show "(SUP P : {P. finite P \<and> P \<subseteq> S'}. emeasure (sup_measure.F id P) X) \<le> emeasure x X"
+            show "(SUP P \<in> {P. finite P \<and> P \<subseteq> S'}. emeasure (sup_measure.F id P) X) \<le> emeasure x X"
             proof (safe intro!: SUP_least)
               fix P assume P: "finite P" "P \<subseteq> S'"
               show "emeasure (sup_measure.F id P) X \<le> emeasure x X"
@@ -3455,7 +3455,7 @@
 
 lemma sets_SUP:
   assumes "\<And>x. x \<in> I \<Longrightarrow> sets (M x) = sets N"
-  shows "I \<noteq> {} \<Longrightarrow> sets (SUP i:I. M i) = sets N"
+  shows "I \<noteq> {} \<Longrightarrow> sets (SUP i\<in>I. M i) = sets N"
   unfolding Sup_measure_def
   using assms assms[THEN sets_eq_imp_space_eq]
     sets_Sup_measure'[where A=N and M="M`I"]
@@ -3463,27 +3463,27 @@
 
 lemma emeasure_SUP:
   assumes sets: "\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sets N" "X \<in> sets N" "I \<noteq> {}"
-  shows "emeasure (SUP i:I. M i) X = (SUP J:{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. emeasure (SUP i:J. M i) X)"
+  shows "emeasure (SUP i\<in>I. M i) X = (SUP J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. emeasure (SUP i\<in>J. M i) X)"
 proof -
   interpret sup_measure: comm_monoid_set sup "bot :: 'b measure"
     by standard (auto intro!: antisym)
-  have eq: "finite J \<Longrightarrow> sup_measure.F id J = (SUP i:J. i)" for J :: "'b measure set"
+  have eq: "finite J \<Longrightarrow> sup_measure.F id J = (SUP i\<in>J. i)" for J :: "'b measure set"
     by (induction J rule: finite_induct) auto
-  have 1: "J \<noteq> {} \<Longrightarrow> J \<subseteq> I \<Longrightarrow> sets (SUP x:J. M x) = sets N" for J
+  have 1: "J \<noteq> {} \<Longrightarrow> J \<subseteq> I \<Longrightarrow> sets (SUP x\<in>J. M x) = sets N" for J
     by (intro sets_SUP sets) (auto )
   from \<open>I \<noteq> {}\<close> obtain i where "i\<in>I" by auto
-  have "Sup_measure' (M`I) X = (SUP P:{P. finite P \<and> P \<subseteq> M`I}. sup_measure.F id P X)"
+  have "Sup_measure' (M`I) X = (SUP P\<in>{P. finite P \<and> P \<subseteq> M`I}. sup_measure.F id P X)"
     using sets by (intro emeasure_Sup_measure') auto
-  also have "Sup_measure' (M`I) = (SUP i:I. M i)"
+  also have "Sup_measure' (M`I) = (SUP i\<in>I. M i)"
     unfolding Sup_measure_def using \<open>I \<noteq> {}\<close> sets sets(1)[THEN sets_eq_imp_space_eq]
     by (intro Sup_lexord1[where P="\<lambda>x. _ = x"]) auto
-  also have "(SUP P:{P. finite P \<and> P \<subseteq> M`I}. sup_measure.F id P X) =
-    (SUP J:{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. (SUP i:J. M i) X)"
+  also have "(SUP P\<in>{P. finite P \<and> P \<subseteq> M`I}. sup_measure.F id P X) =
+    (SUP J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. (SUP i\<in>J. M i) X)"
   proof (intro SUP_eq)
     fix J assume "J \<in> {P. finite P \<and> P \<subseteq> M`I}"
     then obtain J' where J': "J' \<subseteq> I" "finite J'" and J: "J = M`J'" and "finite J"
       using finite_subset_image[of J M I] by auto
-    show "\<exists>j\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. sup_measure.F id J X \<le> (SUP i:j. M i) X"
+    show "\<exists>j\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. sup_measure.F id J X \<le> (SUP i\<in>j. M i) X"
     proof cases
       assume "J' = {}" with \<open>i \<in> I\<close> show ?thesis
         by (auto simp add: J)
@@ -3493,7 +3493,7 @@
     qed
   next
     fix J assume J: "J \<in> {P. P \<noteq> {} \<and> finite P \<and> P \<subseteq> I}"
-    show "\<exists>J'\<in>{J. finite J \<and> J \<subseteq> M`I}. (SUP i:J. M i) X \<le> sup_measure.F id J' X"
+    show "\<exists>J'\<in>{J. finite J \<and> J \<subseteq> M`I}. (SUP i\<in>J. M i) X \<le> sup_measure.F id J' X"
       using J by (intro bexI[of _ "M`J"]) (auto simp add: eq simp del: id_apply)
   qed
   finally show ?thesis .
@@ -3502,14 +3502,14 @@
 lemma emeasure_SUP_chain:
   assumes sets: "\<And>i. i \<in> A \<Longrightarrow> sets (M i) = sets N" "X \<in> sets N"
   assumes ch: "Complete_Partial_Order.chain (\<le>) (M ` A)" and "A \<noteq> {}"
-  shows "emeasure (SUP i:A. M i) X = (SUP i:A. emeasure (M i) X)"
+  shows "emeasure (SUP i\<in>A. M i) X = (SUP i\<in>A. emeasure (M i) X)"
 proof (subst emeasure_SUP[OF sets \<open>A \<noteq> {}\<close>])
-  show "(SUP J:{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> A}. emeasure (SUPREMUM J M) X) = (SUP i:A. emeasure (M i) X)"
+  show "(SUP J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> A}. emeasure (SUPREMUM J M) X) = (SUP i\<in>A. emeasure (M i) X)"
   proof (rule SUP_eq)
     fix J assume "J \<in> {J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> A}"
     then have J: "Complete_Partial_Order.chain (\<le>) (M ` J)" "finite J" "J \<noteq> {}" and "J \<subseteq> A"
       using ch[THEN chain_subset, of "M`J"] by auto
-    with in_chain_finite[OF J(1)] obtain j where "j \<in> J" "(SUP j:J. M j) = M j"
+    with in_chain_finite[OF J(1)] obtain j where "j \<in> J" "(SUP j\<in>J. M j) = M j"
       by auto
     with \<open>J \<subseteq> A\<close> show "\<exists>j\<in>A. emeasure (SUPREMUM J M) X \<le> emeasure (M j) X"
       by auto
@@ -3554,20 +3554,20 @@
 
 lemma Sup_lexord_rel:
   assumes "\<And>i. i \<in> I \<Longrightarrow> k (A i) = k (B i)"
-    "R (c (A ` {a \<in> I. k (B a) = (SUP x:I. k (B x))})) (c (B ` {a \<in> I. k (B a) = (SUP x:I. k (B x))}))"
+    "R (c (A ` {a \<in> I. k (B a) = (SUP x\<in>I. k (B x))})) (c (B ` {a \<in> I. k (B a) = (SUP x\<in>I. k (B x))}))"
     "R (s (A`I)) (s (B`I))"
   shows "R (Sup_lexord k c s (A`I)) (Sup_lexord k c s (B`I))"
 proof -
-  have "A ` {a \<in> I. k (B a) = (SUP x:I. k (B x))} =  {a \<in> A ` I. k a = (SUP x:I. k (B x))}"
+  have "A ` {a \<in> I. k (B a) = (SUP x\<in>I. k (B x))} =  {a \<in> A ` I. k a = (SUP x\<in>I. k (B x))}"
     using assms(1) by auto
-  moreover have "B ` {a \<in> I. k (B a) = (SUP x:I. k (B x))} =  {a \<in> B ` I. k a = (SUP x:I. k (B x))}"
+  moreover have "B ` {a \<in> I. k (B a) = (SUP x\<in>I. k (B x))} =  {a \<in> B ` I. k a = (SUP x\<in>I. k (B x))}"
     by auto
   ultimately show ?thesis
     using assms by (auto simp: Sup_lexord_def Let_def)
 qed
 
 lemma sets_SUP_cong:
-  assumes eq: "\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sets (N i)" shows "sets (SUP i:I. M i) = sets (SUP i:I. N i)"
+  assumes eq: "\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sets (N i)" shows "sets (SUP i\<in>I. M i) = sets (SUP i\<in>I. N i)"
   unfolding Sup_measure_def
   using eq eq[THEN sets_eq_imp_space_eq]
   apply (intro Sup_lexord_rel[where R="\<lambda>x y. sets x = sets y"])
@@ -3627,17 +3627,17 @@
 
 lemma measurable_SUP2:
   "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f \<in> measurable N (M i)) \<Longrightarrow>
-    (\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> space (M i) = space (M j)) \<Longrightarrow> f \<in> measurable N (SUP i:I. M i)"
+    (\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> space (M i) = space (M j)) \<Longrightarrow> f \<in> measurable N (SUP i\<in>I. M i)"
   by (auto intro!: measurable_Sup2)
 
 lemma sets_Sup_sigma:
   assumes [simp]: "M \<noteq> {}" and M: "\<And>m. m \<in> M \<Longrightarrow> m \<subseteq> Pow \<Omega>"
-  shows "sets (SUP m:M. sigma \<Omega> m) = sets (sigma \<Omega> (\<Union>M))"
+  shows "sets (SUP m\<in>M. sigma \<Omega> m) = sets (sigma \<Omega> (\<Union>M))"
 proof -
   { fix a m assume "a \<in> sigma_sets \<Omega> m" "m \<in> M"
     then have "a \<in> sigma_sets \<Omega> (\<Union>M)"
      by induction (auto intro: sigma_sets.intros(2-)) }
-  then show "sets (SUP m:M. sigma \<Omega> m) = sets (sigma \<Omega> (\<Union>M))"
+  then show "sets (SUP m\<in>M. sigma \<Omega> m) = sets (sigma \<Omega> (\<Union>M))"
     apply (subst sets_Sup_eq[where X="\<Omega>"])
     apply (auto simp add: M) []
     apply auto []
@@ -3649,14 +3649,14 @@
 
 lemma Sup_sigma:
   assumes [simp]: "M \<noteq> {}" and M: "\<And>m. m \<in> M \<Longrightarrow> m \<subseteq> Pow \<Omega>"
-  shows "(SUP m:M. sigma \<Omega> m) = (sigma \<Omega> (\<Union>M))"
+  shows "(SUP m\<in>M. sigma \<Omega> m) = (sigma \<Omega> (\<Union>M))"
 proof (intro antisym SUP_least)
   have *: "\<Union>M \<subseteq> Pow \<Omega>"
     using M by auto
-  show "sigma \<Omega> (\<Union>M) \<le> (SUP m:M. sigma \<Omega> m)"
+  show "sigma \<Omega> (\<Union>M) \<le> (SUP m\<in>M. sigma \<Omega> m)"
   proof (intro less_eq_measure.intros(3))
-    show "space (sigma \<Omega> (\<Union>M)) = space (SUP m:M. sigma \<Omega> m)"
-      "sets (sigma \<Omega> (\<Union>M)) = sets (SUP m:M. sigma \<Omega> m)"
+    show "space (sigma \<Omega> (\<Union>M)) = space (SUP m\<in>M. sigma \<Omega> m)"
+      "sets (sigma \<Omega> (\<Union>M)) = sets (SUP m\<in>M. sigma \<Omega> m)"
       using sets_Sup_sigma[OF assms] sets_Sup_sigma[OF assms, THEN sets_eq_imp_space_eq]
       by auto
   qed (simp add: emeasure_sigma le_fun_def)
@@ -3665,12 +3665,12 @@
 qed
 
 lemma SUP_sigma_sigma:
-  "M \<noteq> {} \<Longrightarrow> (\<And>m. m \<in> M \<Longrightarrow> f m \<subseteq> Pow \<Omega>) \<Longrightarrow> (SUP m:M. sigma \<Omega> (f m)) = sigma \<Omega> (\<Union>m\<in>M. f m)"
+  "M \<noteq> {} \<Longrightarrow> (\<And>m. m \<in> M \<Longrightarrow> f m \<subseteq> Pow \<Omega>) \<Longrightarrow> (SUP m\<in>M. sigma \<Omega> (f m)) = sigma \<Omega> (\<Union>m\<in>M. f m)"
   using Sup_sigma[of "f`M" \<Omega>] by auto
 
 lemma sets_vimage_Sup_eq:
   assumes *: "M \<noteq> {}" "f \<in> X \<rightarrow> Y" "\<And>m. m \<in> M \<Longrightarrow> space m = Y"
-  shows "sets (vimage_algebra X f (Sup M)) = sets (SUP m : M. vimage_algebra X f m)"
+  shows "sets (vimage_algebra X f (Sup M)) = sets (SUP m \<in> M. vimage_algebra X f m)"
   (is "?IS = ?SI")
 proof
   show "?IS \<subseteq> ?SI"
@@ -3767,12 +3767,12 @@
     using x by (induct rule: sigma_sets.induct) (insert a, auto)
 qed
 
-lemma in_sets_SUP: "i \<in> I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> space (M i) = Y) \<Longrightarrow> X \<in> sets (M i) \<Longrightarrow> X \<in> sets (SUP i:I. M i)"
+lemma in_sets_SUP: "i \<in> I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> space (M i) = Y) \<Longrightarrow> X \<in> sets (M i) \<Longrightarrow> X \<in> sets (SUP i\<in>I. M i)"
   by (intro in_sets_Sup[where X=Y]) auto
 
 lemma measurable_SUP1:
   "i \<in> I \<Longrightarrow> f \<in> measurable (M i) N \<Longrightarrow> (\<And>m n. m \<in> I \<Longrightarrow> n \<in> I \<Longrightarrow> space (M m) = space (M n)) \<Longrightarrow>
-    f \<in> measurable (SUP i:I. M i) N"
+    f \<in> measurable (SUP i\<in>I. M i) N"
   by (auto intro: measurable_Sup1)
 
 lemma sets_image_in_sets':
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -811,7 +811,7 @@
 subsection \<open>Integral on nonnegative functions\<close>
 
 definition nn_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> ennreal" ("integral\<^sup>N") where
-  "integral\<^sup>N M f = (SUP g : {g. simple_function M g \<and> g \<le> f}. integral\<^sup>S M g)"
+  "integral\<^sup>N M f = (SUP g \<in> {g. simple_function M g \<and> g \<le> f}. integral\<^sup>S M g)"
 
 syntax
   "_nn_integral" :: "pttrn \<Rightarrow> ennreal \<Rightarrow> 'a measure \<Rightarrow> ennreal" ("\<integral>\<^sup>+((2 _./ _)/ \<partial>_)" [60,61] 110)
@@ -820,7 +820,7 @@
   "\<integral>\<^sup>+x. f \<partial>M" == "CONST nn_integral M (\<lambda>x. f)"
 
 lemma nn_integral_def_finite:
-  "integral\<^sup>N M f = (SUP g : {g. simple_function M g \<and> g \<le> f \<and> (\<forall>x. g x < top)}. integral\<^sup>S M g)"
+  "integral\<^sup>N M f = (SUP g \<in> {g. simple_function M g \<and> g \<le> f \<and> (\<forall>x. g x < top)}. integral\<^sup>S M g)"
     (is "_ = SUPREMUM ?A ?f")
   unfolding nn_integral_def
 proof (safe intro!: antisym SUP_least)
@@ -1342,7 +1342,7 @@
   assumes u: "\<And>i. u i \<in> borel_measurable M"
   shows "(\<integral>\<^sup>+ x. liminf (\<lambda>n. u n x) \<partial>M) \<le> liminf (\<lambda>n. integral\<^sup>N M (u n))"
 proof -
-  have "(\<integral>\<^sup>+ x. liminf (\<lambda>n. u n x) \<partial>M) = (SUP n. \<integral>\<^sup>+ x. (INF i:{n..}. u i x) \<partial>M)"
+  have "(\<integral>\<^sup>+ x. liminf (\<lambda>n. u n x) \<partial>M) = (SUP n. \<integral>\<^sup>+ x. (INF i\<in>{n..}. u i x) \<partial>M)"
     unfolding liminf_SUP_INF using u
     by (intro nn_integral_monotone_convergence_SUP_AE)
        (auto intro!: AE_I2 intro: INF_greatest INF_superset_mono)
@@ -1361,7 +1361,7 @@
     using bounds by (auto simp: AE_all_countable)
   then have "(\<integral>\<^sup>+ x. (SUP n. u n x) \<partial>M) \<le> (\<integral>\<^sup>+ x. w x \<partial>M)"
     by (auto intro!: nn_integral_mono_AE elim: eventually_mono intro: SUP_least)
-  then have "(\<integral>\<^sup>+ x. limsup (\<lambda>n. u n x) \<partial>M) = (INF n. \<integral>\<^sup>+ x. (SUP i:{n..}. u i x) \<partial>M)"
+  then have "(\<integral>\<^sup>+ x. limsup (\<lambda>n. u n x) \<partial>M) = (INF n. \<integral>\<^sup>+ x. (SUP i\<in>{n..}. u i x) \<partial>M)"
     unfolding limsup_INF_SUP using bnd w
     by (intro nn_integral_monotone_convergence_INF_AE')
        (auto intro!: AE_I2 intro: SUP_least SUP_subset_mono)
@@ -1875,24 +1875,24 @@
   fixes f :: "'a \<Rightarrow> nat \<Rightarrow> ennreal"
   assumes chain: "Complete_Partial_Order.chain (\<le>) (f ` Y)"
   and nonempty: "Y \<noteq> {}"
-  shows "(\<integral>\<^sup>+ x. (SUP i:Y. f i x) \<partial>count_space UNIV) = (SUP i:Y. (\<integral>\<^sup>+ x. f i x \<partial>count_space UNIV))"
+  shows "(\<integral>\<^sup>+ x. (SUP i\<in>Y. f i x) \<partial>count_space UNIV) = (SUP i\<in>Y. (\<integral>\<^sup>+ x. f i x \<partial>count_space UNIV))"
   (is "?lhs = ?rhs" is "integral\<^sup>N ?M _ = _")
 proof (rule order_class.order.antisym)
   show "?rhs \<le> ?lhs"
     by (auto intro!: SUP_least SUP_upper nn_integral_mono)
 next
-  have "\<exists>g. incseq g \<and> range g \<subseteq> (\<lambda>i. f i x) ` Y \<and> (SUP i:Y. f i x) = (SUP i. g i)" for x
+  have "\<exists>g. incseq g \<and> range g \<subseteq> (\<lambda>i. f i x) ` Y \<and> (SUP i\<in>Y. f i x) = (SUP i. g i)" for x
     by (rule ennreal_Sup_countable_SUP) (simp add: nonempty)
   then obtain g where incseq: "\<And>x. incseq (g x)"
     and range: "\<And>x. range (g x) \<subseteq> (\<lambda>i. f i x) ` Y"
-    and sup: "\<And>x. (SUP i:Y. f i x) = (SUP i. g x i)" by moura
+    and sup: "\<And>x. (SUP i\<in>Y. f i x) = (SUP i. g x i)" by moura
   from incseq have incseq': "incseq (\<lambda>i x. g x i)"
     by(blast intro: incseq_SucI le_funI dest: incseq_SucD)
 
   have "?lhs = \<integral>\<^sup>+ x. (SUP i. g x i) \<partial>?M" by(simp add: sup)
   also have "\<dots> = (SUP i. \<integral>\<^sup>+ x. g x i \<partial>?M)" using incseq'
     by(rule nn_integral_monotone_convergence_SUP) simp
-  also have "\<dots> \<le> (SUP i:Y. \<integral>\<^sup>+ x. f i x \<partial>?M)"
+  also have "\<dots> \<le> (SUP i\<in>Y. \<integral>\<^sup>+ x. f i x \<partial>?M)"
   proof(rule SUP_least)
     fix n
     have "\<And>x. \<exists>i. g x n = f i x \<and> i \<in> Y" using range by blast
@@ -1902,7 +1902,7 @@
       by(rule nn_integral_count_space_nat)
     also have "\<dots> = (SUP m. \<Sum>x<m. g x n)"
       by(rule suminf_eq_SUP)
-    also have "\<dots> \<le> (SUP i:Y. \<integral>\<^sup>+ x. f i x \<partial>?M)"
+    also have "\<dots> \<le> (SUP i\<in>Y. \<integral>\<^sup>+ x. f i x \<partial>?M)"
     proof(rule SUP_mono)
       fix m
       show "\<exists>m'\<in>Y. (\<Sum>x<m. g x n) \<le> (\<integral>\<^sup>+ x. f m' x \<partial>?M)"
@@ -1916,7 +1916,7 @@
         with chain have chain': "Complete_Partial_Order.chain (\<le>) (f ` ?Y)" by(rule chain_subset)
         hence "Sup (f ` ?Y) \<in> f ` ?Y"
           by(rule ccpo_class.in_chain_finite)(auto simp add: True lessThan_empty_iff)
-        then obtain m' where "m' < m" and m': "(SUP i:?Y. f i) = f (I m')" by auto
+        then obtain m' where "m' < m" and m': "(SUP i\<in>?Y. f i) = f (I m')" by auto
         have "I m' \<in> Y" using I by blast
         have "(\<Sum>x<m. g x n) \<le> (\<Sum>x<m. f (I m') x)"
         proof(rule sum_mono)
@@ -1924,7 +1924,7 @@
           assume "x \<in> {..<m}"
           hence "x < m" by simp
           have "g x n = f (I x) x" by(simp add: I)
-          also have "\<dots> \<le> (SUP i:?Y. f i) x" unfolding Sup_fun_def image_image
+          also have "\<dots> \<le> (SUP i\<in>?Y. f i) x" unfolding Sup_fun_def image_image
             using \<open>x \<in> {..<m}\<close> by (rule Sup_upper [OF imageI])
           also have "\<dots> = f (I m') x" unfolding m' by simp
           finally show "g x n \<le> f (I m') x" .
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Analysis/Ordered_Euclidean_Space.thy
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -11,8 +11,8 @@
   assumes eucl_less_le_not_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
   assumes eucl_inf: "inf x y = (\<Sum>i\<in>Basis. inf (x \<bullet> i) (y \<bullet> i) *\<^sub>R i)"
   assumes eucl_sup: "sup x y = (\<Sum>i\<in>Basis. sup (x \<bullet> i) (y \<bullet> i) *\<^sub>R i)"
-  assumes eucl_Inf: "Inf X = (\<Sum>i\<in>Basis. (INF x:X. x \<bullet> i) *\<^sub>R i)"
-  assumes eucl_Sup: "Sup X = (\<Sum>i\<in>Basis. (SUP x:X. x \<bullet> i) *\<^sub>R i)"
+  assumes eucl_Inf: "Inf X = (\<Sum>i\<in>Basis. (INF x\<in>X. x \<bullet> i) *\<^sub>R i)"
+  assumes eucl_Sup: "Sup X = (\<Sum>i\<in>Basis. (SUP x\<in>X. x \<bullet> i) *\<^sub>R i)"
   assumes eucl_abs: "\<bar>x\<bar> = (\<Sum>i\<in>Basis. \<bar>x \<bullet> i\<bar> *\<^sub>R i)"
 begin
 
@@ -49,8 +49,8 @@
   by (simp_all add: eucl_inf eucl_sup inner_sum_left inner_Basis if_distrib comm_monoid_add_class.sum.delta
       cong: if_cong)
 
-lemma%unimportant inner_Basis_INF_left: "i \<in> Basis \<Longrightarrow> (INF x:X. f x) \<bullet> i = (INF x:X. f x \<bullet> i)"
-  and inner_Basis_SUP_left: "i \<in> Basis \<Longrightarrow> (SUP x:X. f x) \<bullet> i = (SUP x:X. f x \<bullet> i)"
+lemma%unimportant inner_Basis_INF_left: "i \<in> Basis \<Longrightarrow> (INF x\<in>X. f x) \<bullet> i = (INF x\<in>X. f x \<bullet> i)"
+  and inner_Basis_SUP_left: "i \<in> Basis \<Longrightarrow> (SUP x\<in>X. f x) \<bullet> i = (SUP x\<in>X. f x \<bullet> i)"
   using eucl_Sup [of "f ` X"] eucl_Inf [of "f ` X"] by (simp_all add: comp_def)
 
 lemma%unimportant abs_inner: "i \<in> Basis \<Longrightarrow> \<bar>x\<bar> \<bullet> i = \<bar>x \<bullet> i\<bar>"
@@ -284,8 +284,8 @@
 
 definition%important "inf x y = (\<chi> i. inf (x $ i) (y $ i))"
 definition%important "sup x y = (\<chi> i. sup (x $ i) (y $ i))"
-definition%important "Inf X = (\<chi> i. (INF x:X. x $ i))"
-definition%important "Sup X = (\<chi> i. (SUP x:X. x $ i))"
+definition%important "Inf X = (\<chi> i. (INF x\<in>X. x $ i))"
+definition%important "Sup X = (\<chi> i. (SUP x\<in>X. x $ i))"
 definition%important "\<bar>x\<bar> = (\<chi> i. \<bar>x $ i\<bar>)"
 
 instance
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Analysis/Polytope.thy
--- a/src/HOL/Analysis/Polytope.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Polytope.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -2080,7 +2080,7 @@
           case False
           then obtain h' where h': "h' \<in> F - {h}" by auto
           define inff where "inff =
-            (INF j:F - {h}.
+            (INF j\<in>F - {h}.
               if 0 < a j \<bullet> y - a j \<bullet> w
               then (b j - a j \<bullet> w) / (a j \<bullet> y - a j \<bullet> w)
               else 1)"
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Analysis/Product_Vector.thy
--- a/src/HOL/Analysis/Product_Vector.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Product_Vector.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -127,7 +127,7 @@
 
 definition [code del]:
   "(uniformity :: (('a \<times> 'b) \<times> ('a \<times> 'b)) filter) =
-    (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+    (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})"
 
 instance
   by standard (rule uniformity_prod_def)
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Analysis/Radon_Nikodym.thy
--- a/src/HOL/Analysis/Radon_Nikodym.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Radon_Nikodym.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -254,7 +254,7 @@
         using f \<open>A \<in> sets M\<close> by (auto intro!: SUP_least simp: G_D)
     qed }
   note SUP_in_G = this
-  let ?y = "SUP g : G. integral\<^sup>N M g"
+  let ?y = "SUP g \<in> G. integral\<^sup>N M g"
   have y_le: "?y \<le> N (space M)" unfolding G_def
   proof (safe intro!: SUP_least)
     fix g assume "\<forall>A\<in>sets M. (\<integral>\<^sup>+x. g x * indicator A x \<partial>M) \<le> N A"
@@ -390,7 +390,7 @@
     (\<forall>A\<in>sets M. A \<inter> (\<Union>i. B i) = {} \<longrightarrow> (emeasure M A = 0 \<and> N A = 0) \<or> (emeasure M A > 0 \<and> N A = \<infinity>))"
 proof%unimportant -
   let ?Q = "{Q\<in>sets M. N Q \<noteq> \<infinity>}"
-  let ?a = "SUP Q:?Q. emeasure M Q"
+  let ?a = "SUP Q\<in>?Q. emeasure M Q"
   have "{} \<in> ?Q" by auto
   then have Q_not_empty: "?Q \<noteq> {}" by blast
   have "?a \<le> emeasure M (space M)" using sets.sets_into_space
@@ -404,7 +404,7 @@
   then have "\<forall>i. \<exists>Q'. Q'' i = emeasure M Q' \<and> Q' \<in> ?Q" by auto
   from choice[OF this] obtain Q' where Q': "\<And>i. Q'' i = emeasure M (Q' i)" "\<And>i. Q' i \<in> ?Q"
     by auto
-  then have a_Lim: "?a = (SUP i::nat. emeasure M (Q' i))" using a by simp
+  then have a_Lim: "?a = (SUP i. emeasure M (Q' i))" using a by simp
   let ?O = "\<lambda>n. \<Union>i\<le>n. Q' i"
   have Union: "(SUP i. emeasure M (?O i)) = emeasure M (\<Union>i. ?O i)"
   proof (rule SUP_emeasure_incseq[of ?O])
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Analysis/Regularity.thy
--- a/src/HOL/Analysis/Regularity.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Regularity.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -14,9 +14,9 @@
   assumes "emeasure M (space M) \<noteq> \<infinity>"
   assumes "B \<in> sets borel"
   shows inner_regular: "emeasure M B =
-    (SUP K : {K. K \<subseteq> B \<and> compact K}. emeasure M K)" (is "?inner B")
+    (SUP K \<in> {K. K \<subseteq> B \<and> compact K}. emeasure M K)" (is "?inner B")
   and outer_regular: "emeasure M B =
-    (INF U : {U. B \<subseteq> U \<and> open U}. emeasure M U)" (is "?outer B")
+    (INF U \<in> {U. B \<subseteq> U \<and> open U}. emeasure M U)" (is "?outer B")
 proof%unimportant -
   have Us: "UNIV = space M" by (metis assms(1) sets_eq_imp_space_eq space_borel)
   hence sU: "space M = UNIV" by simp
@@ -183,7 +183,7 @@
       finally
       have "emeasure M A = (INF n. emeasure M {x. infdist x A < 1 / real (Suc n)})" .
       moreover
-      have "\<dots> \<ge> (INF U:{U. A \<subseteq> U \<and> open U}. emeasure M U)"
+      have "\<dots> \<ge> (INF U\<in>{U. A \<subseteq> U \<and> open U}. emeasure M U)"
       proof (intro INF_mono)
         fix m
         have "?G (1 / real (Suc m)) \<in> {U. A \<subseteq> U \<and> open U}" using open_G by auto
@@ -193,7 +193,7 @@
           by blast
       qed
       moreover
-      have "emeasure M A \<le> (INF U:{U. A \<subseteq> U \<and> open U}. emeasure M U)"
+      have "emeasure M A \<le> (INF U\<in>{U. A \<subseteq> U \<and> open U}. emeasure M U)"
         by (rule INF_greatest) (auto intro!: emeasure_mono simp: sb)
       ultimately show ?thesis by simp
     qed (auto intro!: INF_eqI)
@@ -217,38 +217,38 @@
     from compl have [simp]: "B \<in> sets M" by (auto simp: sb borel_eq_closed)
     case 2
     have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl)
-    also have "\<dots> = (INF K:{K. K \<subseteq> B \<and> compact K}. M (space M) -  M K)"
+    also have "\<dots> = (INF K\<in>{K. K \<subseteq> B \<and> compact K}. M (space M) -  M K)"
       by (subst ennreal_SUP_const_minus) (auto simp: less_top[symmetric] inner)
-    also have "\<dots> = (INF U:{U. U \<subseteq> B \<and> compact U}. M (space M - U))"
+    also have "\<dots> = (INF U\<in>{U. U \<subseteq> B \<and> compact U}. M (space M - U))"
       by (rule INF_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
-    also have "\<dots> \<ge> (INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U))"
+    also have "\<dots> \<ge> (INF U\<in>{U. U \<subseteq> B \<and> closed U}. M (space M - U))"
       by (rule INF_superset_mono) (auto simp add: compact_imp_closed)
-    also have "(INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U)) =
-        (INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U)"
+    also have "(INF U\<in>{U. U \<subseteq> B \<and> closed U}. M (space M - U)) =
+        (INF U\<in>{U. space M - B \<subseteq> U \<and> open U}. emeasure M U)"
       unfolding INF_image [of _ "\<lambda>u. space M - u" _, symmetric, unfolded comp_def]
         by (rule INF_cong) (auto simp add: sU Compl_eq_Diff_UNIV [symmetric, simp])
     finally have
-      "(INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<le> emeasure M (space M - B)" .
+      "(INF U\<in>{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<le> emeasure M (space M - B)" .
     moreover have
-      "(INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<ge> emeasure M (space M - B)"
+      "(INF U\<in>{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<ge> emeasure M (space M - B)"
       by (auto simp: sb sU intro!: INF_greatest emeasure_mono)
     ultimately show ?case by (auto intro!: antisym simp: sets_eq_imp_space_eq[OF sb])
 
     case 1
     have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl)
-    also have "\<dots> = (SUP U: {U. B \<subseteq> U \<and> open U}. M (space M) -  M U)"
+    also have "\<dots> = (SUP U\<in> {U. B \<subseteq> U \<and> open U}. M (space M) -  M U)"
       unfolding outer by (subst ennreal_INF_const_minus) auto
-    also have "\<dots> = (SUP U:{U. B \<subseteq> U \<and> open U}. M (space M - U))"
+    also have "\<dots> = (SUP U\<in>{U. B \<subseteq> U \<and> open U}. M (space M - U))"
       by (rule SUP_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
-    also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> closed K}. emeasure M K)"
+    also have "\<dots> = (SUP K\<in>{K. K \<subseteq> space M - B \<and> closed K}. emeasure M K)"
       unfolding SUP_image [of _ "\<lambda>u. space M - u" _, symmetric, unfolded comp_def]
         by (rule SUP_cong) (auto simp add: sU)
-    also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)"
+    also have "\<dots> = (SUP K\<in>{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)"
     proof (safe intro!: antisym SUP_least)
       fix K assume "closed K" "K \<subseteq> space M - B"
       from closed_in_D[OF \<open>closed K\<close>]
-      have K_inner: "emeasure M K = (SUP K:{Ka. Ka \<subseteq> K \<and> compact Ka}. emeasure M K)" by simp
-      show "emeasure M K \<le> (SUP K:{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)"
+      have K_inner: "emeasure M K = (SUP K\<in>{Ka. Ka \<subseteq> K \<and> compact Ka}. emeasure M K)" by simp
+      show "emeasure M K \<le> (SUP K\<in>{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)"
         unfolding K_inner using \<open>K \<subseteq> space M - B\<close>
         by (auto intro!: SUP_upper SUP_least)
     qed (fastforce intro!: SUP_least SUP_upper simp: compact_imp_closed)
@@ -284,7 +284,7 @@
       proof
         fix i
         from \<open>0 < e\<close> have "0 < e/(2*Suc n0)" by simp
-        have "emeasure M (D i) = (SUP K:{K. K \<subseteq> (D i) \<and> compact K}. emeasure M K)"
+        have "emeasure M (D i) = (SUP K\<in>{K. K \<subseteq> (D i) \<and> compact K}. emeasure M K)"
           using union by blast
         from SUP_approx_ennreal[OF \<open>0 < e/(2*Suc n0)\<close> _ this]
         show "\<exists>K. K \<subseteq> D i \<and> compact K \<and> emeasure M (D i) \<le> emeasure M K + e/(2*Suc n0)"
@@ -327,7 +327,7 @@
       proof
         fix i::nat
         from \<open>0 < e\<close> have "0 < e/(2 powr Suc i)" by simp
-        have "emeasure M (D i) = (INF U:{U. (D i) \<subseteq> U \<and> open U}. emeasure M U)"
+        have "emeasure M (D i) = (INF U\<in>{U. (D i) \<subseteq> U \<and> open U}. emeasure M U)"
           using union by blast
         from INF_approx_ennreal[OF \<open>0 < e/(2 powr Suc i)\<close> this]
         show "\<exists>U. D i \<subseteq> U \<and> open U \<and> e/(2 powr Suc i) > emeasure M U - emeasure M (D i)"
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Analysis/Riemann_Mapping.thy
--- a/src/HOL/Analysis/Riemann_Mapping.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Riemann_Mapping.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -168,7 +168,7 @@
           by (simp add: deq norm_mult divide_simps o_def)
       qed
     qed
-    define l where "l \<equiv> SUP h:F. norm (deriv h 0)"
+    define l where "l \<equiv> SUP h\<in>F. norm (deriv h 0)"
     have eql: "norm (deriv f 0) = l" if le: "l \<le> norm (deriv f 0)" and "f \<in> F" for f
       apply (rule order_antisym [OF _ le])
       using \<open>f \<in> F\<close> bdd cSUP_upper by (fastforce simp: l_def)
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Analysis/Tagged_Division.thy
--- a/src/HOL/Analysis/Tagged_Division.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Tagged_Division.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -133,10 +133,10 @@
 subsection%important \<open>Bounds on intervals where they exist\<close>
 
 definition%important interval_upperbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
-  where "interval_upperbound s = (\<Sum>i\<in>Basis. (SUP x:s. x\<bullet>i) *\<^sub>R i)"
+  where "interval_upperbound s = (\<Sum>i\<in>Basis. (SUP x\<in>s. x\<bullet>i) *\<^sub>R i)"
 
 definition%important interval_lowerbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
-  where "interval_lowerbound s = (\<Sum>i\<in>Basis. (INF x:s. x\<bullet>i) *\<^sub>R i)"
+  where "interval_lowerbound s = (\<Sum>i\<in>Basis. (INF x\<in>s. x\<bullet>i) *\<^sub>R i)"
 
 lemma interval_upperbound[simp]:
   "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
@@ -169,10 +169,10 @@
   shows "interval_upperbound (A \<times> B) = (interval_upperbound A, interval_upperbound B)"
 proof%unimportant-
   from assms have fst_image_times': "A = fst ` (A \<times> B)" by simp
-  have "(\<Sum>i\<in>Basis. (SUP x:A \<times> B. x \<bullet> (i, 0)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (SUP x:A. x \<bullet> i) *\<^sub>R i)"
+  have "(\<Sum>i\<in>Basis. (SUP x\<in>A \<times> B. x \<bullet> (i, 0)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (SUP x\<in>A. x \<bullet> i) *\<^sub>R i)"
       by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0)
   moreover from assms have snd_image_times': "B = snd ` (A \<times> B)" by simp
-  have "(\<Sum>i\<in>Basis. (SUP x:A \<times> B. x \<bullet> (0, i)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (SUP x:B. x \<bullet> i) *\<^sub>R i)"
+  have "(\<Sum>i\<in>Basis. (SUP x\<in>A \<times> B. x \<bullet> (0, i)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (SUP x\<in>B. x \<bullet> i) *\<^sub>R i)"
       by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0)
   ultimately show ?thesis unfolding interval_upperbound_def
       by (subst sum_Basis_prod_eq) (auto simp add: sum_prod)
@@ -183,10 +183,10 @@
   shows "interval_lowerbound (A \<times> B) = (interval_lowerbound A, interval_lowerbound B)"
 proof%unimportant-
   from assms have fst_image_times': "A = fst ` (A \<times> B)" by simp
-  have "(\<Sum>i\<in>Basis. (INF x:A \<times> B. x \<bullet> (i, 0)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (INF x:A. x \<bullet> i) *\<^sub>R i)"
+  have "(\<Sum>i\<in>Basis. (INF x\<in>A \<times> B. x \<bullet> (i, 0)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (INF x\<in>A. x \<bullet> i) *\<^sub>R i)"
       by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0)
   moreover from assms have snd_image_times': "B = snd ` (A \<times> B)" by simp
-  have "(\<Sum>i\<in>Basis. (INF x:A \<times> B. x \<bullet> (0, i)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (INF x:B. x \<bullet> i) *\<^sub>R i)"
+  have "(\<Sum>i\<in>Basis. (INF x\<in>A \<times> B. x \<bullet> (0, i)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (INF x\<in>B. x \<bullet> i) *\<^sub>R i)"
       by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0)
   ultimately show ?thesis unfolding interval_lowerbound_def
       by (subst sum_Basis_prod_eq) (auto simp add: sum_prod)
@@ -2576,7 +2576,7 @@
 text \<open>Divisions over all gauges towards finer divisions.\<close>
 
 definition%important division_filter :: "'a::euclidean_space set \<Rightarrow> ('a \<times> 'a set) set filter"
-  where "division_filter s = (INF g:{g. gauge g}. principal {p. p tagged_division_of s \<and> g fine p})"
+  where "division_filter s = (INF g\<in>{g. gauge g}. principal {p. p tagged_division_of s \<and> g fine p})"
 
 lemma%important eventually_division_filter:
   "(\<forall>\<^sub>F p in division_filter s. P p) \<longleftrightarrow>
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -4189,7 +4189,7 @@
 next
   fix A
   assume A: "\<forall>a\<in>A. closed a" "\<forall>B\<subseteq>A. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {}" "U \<inter> \<Inter>A = {}"
-  define F where "F = (INF a:insert U A. principal a)"
+  define F where "F = (INF a\<in>insert U A. principal a)"
   have "F \<noteq> bot"
     unfolding F_def
   proof (rule INF_filter_not_bot)
@@ -4197,7 +4197,7 @@
     assume X: "X \<subseteq> insert U A" "finite X"
     with A(2)[THEN spec, of "X - {U}"] have "U \<inter> \<Inter>(X - {U}) \<noteq> {}"
       by auto
-    with X show "(INF a:X. principal a) \<noteq> bot"
+    with X show "(INF a\<in>X. principal a) \<noteq> bot"
       by (auto simp: INF_principal_finite principal_eq_bot_iff)
   qed
   moreover
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Analysis/Uniform_Limit.thy
--- a/src/HOL/Analysis/Uniform_Limit.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Uniform_Limit.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -13,7 +13,7 @@
 subsection \<open>Definition\<close>
 
 definition%important uniformly_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::metric_space) \<Rightarrow> ('a \<Rightarrow> 'b) filter"
-  where "uniformly_on S l = (INF e:{0 <..}. principal {f. \<forall>x\<in>S. dist (f x) (l x) < e})"
+  where "uniformly_on S l = (INF e\<in>{0 <..}. principal {f. \<forall>x\<in>S. dist (f x) (l x) < e})"
 
 abbreviation%important
   "uniform_limit S f l \<equiv> filterlim f (uniformly_on S l)"
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Analysis/Weierstrass_Theorems.thy
--- a/src/HOL/Analysis/Weierstrass_Theorems.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Weierstrass_Theorems.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -202,7 +202,7 @@
     by (induct I rule: finite_induct; simp add: const mult)
 
   definition%important normf :: "('a::t2_space \<Rightarrow> real) \<Rightarrow> real"
-    where "normf f \<equiv> SUP x:S. \<bar>f x\<bar>"
+    where "normf f \<equiv> SUP x\<in>S. \<bar>f x\<bar>"
 
   lemma%unimportant normf_upper: "\<lbrakk>continuous_on S f; x \<in> S\<rbrakk> \<Longrightarrow> \<bar>f x\<bar> \<le> normf f"
     apply (simp add: normf_def)
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Complete_Lattices.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -32,12 +32,6 @@
 
 end
 
-syntax (input)
-  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3INF _./ _)" [0, 10] 10)
-  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3INF _:_./ _)" [0, 0, 10] 10)
-  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3SUP _./ _)" [0, 10] 10)
-  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3SUP _:_./ _)" [0, 0, 10] 10)
-
 syntax
   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3INF _./ _)" [0, 10] 10)
   "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3INF _\<in>_./ _)" [0, 0, 10] 10)
@@ -50,6 +44,12 @@
   "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
   "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
 
+syntax (input) \<comment> \<open>legacy input syntax\<close>
+  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3INF _./ _)" [0, 10] 10)
+  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3INF _:_./ _)" [0, 0, 10] 10)
+  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3SUP _./ _)" [0, 10] 10)
+  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3SUP _:_./ _)" [0, 0, 10] 10)
+
 translations
   "\<Sqinter>x y. f"   \<rightleftharpoons> "\<Sqinter>x. \<Sqinter>y. f"
   "\<Sqinter>x. f"     \<rightleftharpoons> "\<Sqinter>CONST range (\<lambda>x. f)"
@@ -236,7 +236,7 @@
 lemma INF_mono: "(\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<le> g m) \<Longrightarrow> (\<Sqinter>n\<in>A. f n) \<le> (\<Sqinter>n\<in>B. g n)"
   using Inf_mono [of "g ` B" "f ` A"] by auto
 
-lemma INF_mono': "(\<And>x. f x \<le> g x) \<Longrightarrow> (INF x:A. f x) \<le> (INF x:A. g x)"
+lemma INF_mono': "(\<And>x. f x \<le> g x) \<Longrightarrow> (\<Sqinter>x\<in>A. f x) \<le> (\<Sqinter>x\<in>A. g x)"
   by (rule INF_mono) auto
 
 lemma Sup_mono:
@@ -252,7 +252,7 @@
 lemma SUP_mono: "(\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<le> g m) \<Longrightarrow> (\<Squnion>n\<in>A. f n) \<le> (\<Squnion>n\<in>B. g n)"
   using Sup_mono [of "f ` A" "g ` B"] by auto
 
-lemma SUP_mono': "(\<And>x. f x \<le> g x) \<Longrightarrow> (SUP x:A. f x) \<le> (SUP x:A. g x)"
+lemma SUP_mono': "(\<And>x. f x \<le> g x) \<Longrightarrow> (\<Squnion>x\<in>A. f x) \<le> (\<Squnion>x\<in>A. g x)"
   by (rule SUP_mono) auto
 
 lemma INF_superset_mono: "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (\<Sqinter>x\<in>A. f x) \<le> (\<Sqinter>x\<in>B. g x)"
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Complex.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -308,7 +308,7 @@
 definition dist_complex_def: "dist x y = cmod (x - y)"
 
 definition uniformity_complex_def [code del]:
-  "(uniformity :: (complex \<times> complex) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+  "(uniformity :: (complex \<times> complex) filter) = (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})"
 
 definition open_complex_def [code del]:
   "open (U :: complex set) \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Computational_Algebra/Formal_Power_Series.thy
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -821,7 +821,7 @@
 begin
 
 definition uniformity_fps_def [code del]:
-  "(uniformity :: ('a fps \<times> 'a fps) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+  "(uniformity :: ('a fps \<times> 'a fps) filter) = (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})"
 
 definition open_fps_def' [code del]:
   "open (U :: 'a fps set) \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
@@ -1470,40 +1470,40 @@
 
 lemma fps_Gcd:
   assumes "A - {0} \<noteq> {}"
-  shows   "Gcd A = fps_X ^ (INF f:A-{0}. subdegree f)"
+  shows   "Gcd A = fps_X ^ (INF f\<in>A-{0}. subdegree f)"
 proof (rule sym, rule GcdI)
   fix f assume "f \<in> A"
-  thus "fps_X ^ (INF f:A - {0}. subdegree f) dvd f"
+  thus "fps_X ^ (INF f\<in>A - {0}. subdegree f) dvd f"
     by (cases "f = 0") (auto simp: fps_dvd_iff intro!: cINF_lower)
 next
   fix d assume d: "\<And>f. f \<in> A \<Longrightarrow> d dvd f"
   from assms obtain f where "f \<in> A - {0}" by auto
   with d[of f] have [simp]: "d \<noteq> 0" by auto
-  from d assms have "subdegree d \<le> (INF f:A-{0}. subdegree f)"
+  from d assms have "subdegree d \<le> (INF f\<in>A-{0}. subdegree f)"
     by (intro cINF_greatest) (auto simp: fps_dvd_iff[symmetric])
-  with d assms show "d dvd fps_X ^ (INF f:A-{0}. subdegree f)" by (simp add: fps_dvd_iff)
+  with d assms show "d dvd fps_X ^ (INF f\<in>A-{0}. subdegree f)" by (simp add: fps_dvd_iff)
 qed simp_all
 
 lemma fps_Gcd_altdef: "Gcd (A :: 'a :: field fps set) =
-  (if A \<subseteq> {0} then 0 else fps_X ^ (INF f:A-{0}. subdegree f))"
+  (if A \<subseteq> {0} then 0 else fps_X ^ (INF f\<in>A-{0}. subdegree f))"
   using fps_Gcd by auto
 
 lemma fps_Lcm:
   assumes "A \<noteq> {}" "0 \<notin> A" "bdd_above (subdegree`A)"
-  shows   "Lcm A = fps_X ^ (SUP f:A. subdegree f)"
+  shows   "Lcm A = fps_X ^ (SUP f\<in>A. subdegree f)"
 proof (rule sym, rule LcmI)
   fix f assume "f \<in> A"
   moreover from assms(3) have "bdd_above (subdegree ` A)" by auto
-  ultimately show "f dvd fps_X ^ (SUP f:A. subdegree f)" using assms(2)
+  ultimately show "f dvd fps_X ^ (SUP f\<in>A. subdegree f)" using assms(2)
     by (cases "f = 0") (auto simp: fps_dvd_iff intro!: cSUP_upper)
 next
   fix d assume d: "\<And>f. f \<in> A \<Longrightarrow> f dvd d"
   from assms obtain f where f: "f \<in> A" "f \<noteq> 0" by auto
-  show "fps_X ^ (SUP f:A. subdegree f) dvd d"
+  show "fps_X ^ (SUP f\<in>A. subdegree f) dvd d"
   proof (cases "d = 0")
     assume "d \<noteq> 0"
     moreover from d have "\<And>f. f \<in> A \<Longrightarrow> f \<noteq> 0 \<Longrightarrow> f dvd d" by blast
-    ultimately have "subdegree d \<ge> (SUP f:A. subdegree f)" using assms
+    ultimately have "subdegree d \<ge> (SUP f\<in>A. subdegree f)" using assms
       by (intro cSUP_least) (auto simp: fps_dvd_iff)
     with \<open>d \<noteq> 0\<close> show ?thesis by (simp add: fps_dvd_iff)
   qed simp_all
@@ -1512,7 +1512,7 @@
 lemma fps_Lcm_altdef:
   "Lcm (A :: 'a :: field fps set) =
      (if 0 \<in> A \<or> \<not>bdd_above (subdegree`A) then 0 else
-      if A = {} then 1 else fps_X ^ (SUP f:A. subdegree f))"
+      if A = {} then 1 else fps_X ^ (SUP f\<in>A. subdegree f))"
 proof (cases "bdd_above (subdegree`A)")
   assume unbounded: "\<not>bdd_above (subdegree`A)"
   have "Lcm A = 0"
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Filter.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -524,14 +524,14 @@
 
 lemma eventually_INF_finite:
   assumes "finite A"
-  shows   "eventually P (INF x:A. F x) \<longleftrightarrow>
+  shows   "eventually P (\<Sqinter> x\<in>A. F x) \<longleftrightarrow>
              (\<exists>Q. (\<forall>x\<in>A. eventually (Q x) (F x)) \<and> (\<forall>y. (\<forall>x\<in>A. Q x y) \<longrightarrow> P y))" 
   using assms
 proof (induction arbitrary: P rule: finite_induct)
   case (insert a A P)
   from insert.hyps have [simp]: "x \<noteq> a" if "x \<in> A" for x
     using that by auto
-  have "eventually P (INF x:insert a A. F x) \<longleftrightarrow>
+  have "eventually P (\<Sqinter> x\<in>insert a A. F x) \<longleftrightarrow>
           (\<exists>Q R S. eventually Q (F a) \<and> (( (\<forall>x\<in>A. eventually (S x) (F x)) \<and>
             (\<forall>y. (\<forall>x\<in>A. S x y) \<longrightarrow> R y)) \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x)))"
     unfolding ex_simps by (simp add: eventually_inf insert.IH)
@@ -915,7 +915,7 @@
 subsection \<open>Increasing finite subsets\<close>
 
 definition finite_subsets_at_top where
-  "finite_subsets_at_top A = (INF X:{X. finite X \<and> X \<subseteq> A}. principal {Y. finite Y \<and> X \<subseteq> Y \<and> Y \<subseteq> A})"
+  "finite_subsets_at_top A = (\<Sqinter> X\<in>{X. finite X \<and> X \<subseteq> A}. principal {Y. finite Y \<and> X \<subseteq> Y \<and> Y \<subseteq> A})"
 
 lemma eventually_finite_subsets_at_top:
   "eventually P (finite_subsets_at_top A) \<longleftrightarrow>
@@ -1345,7 +1345,7 @@
   "(\<And>m. m \<in> J \<Longrightarrow> \<exists>i\<in>I. filtermap f (F i) \<le> G m) \<Longrightarrow> LIM x (\<Sqinter>i\<in>I. F i). f x :> (\<Sqinter>j\<in>J. G j)"
   unfolding filterlim_def by (rule order_trans[OF filtermap_INF INF_mono])
 
-lemma filterlim_INF': "x \<in> A \<Longrightarrow> filterlim f F (G x) \<Longrightarrow> filterlim f F (INF x:A. G x)"
+lemma filterlim_INF': "x \<in> A \<Longrightarrow> filterlim f F (G x) \<Longrightarrow> filterlim f F (\<Sqinter> x\<in>A. G x)"
   unfolding filterlim_def by (rule order.trans[OF filtermap_mono[OF INF_lower]])
 
 lemma filterlim_filtercomap_iff: "filterlim f (filtercomap g G) F \<longleftrightarrow> filterlim (g \<circ> f) G F"
@@ -1859,7 +1859,7 @@
     if "(F, G) \<in> SS'" for P Q F G by simp_all
   show "rel_filter A (Sup S) (Sup S')"
   proof
-    let ?Z = "SUP (F, G):SS'. Z F G"
+    let ?Z = "\<Squnion>(F, G)\<in>SS'. Z F G"
     show *: "\<forall>\<^sub>F (x, y) in ?Z. A x y" using Z by(auto simp add: eventually_Sup)
     show "map_filter_on {(x, y). A x y} fst ?Z = Sup S" "map_filter_on {(x, y). A x y} snd ?Z = Sup S'"
       unfolding filter_eq_iff
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/IMP/Collecting.thy
--- a/src/HOL/IMP/Collecting.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/IMP/Collecting.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -94,7 +94,7 @@
      dest: size_annos_same)
 
 definition Inf_acom :: "com \<Rightarrow> 'a::complete_lattice acom set \<Rightarrow> 'a acom" where
-"Inf_acom c M = annotate (\<lambda>p. INF C:M. anno C p) c"
+"Inf_acom c M = annotate (\<lambda>p. INF C\<in>M. anno C p) c"
 
 global_interpretation
   Complete_Lattice "{C. strip C = c}" "Inf_acom c" for c
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Library/Countable_Complete_Lattices.thy
--- a/src/HOL/Library/Countable_Complete_Lattices.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Library/Countable_Complete_Lattices.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -27,58 +27,58 @@
   show "a \<le> top" by (auto intro: ccInf_greatest simp only: ccInf_empty [symmetric])
 qed
 
-lemma ccINF_lower: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> (INF i :A. f i) \<le> f i"
+lemma ccINF_lower: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> (INF i \<in> A. f i) \<le> f i"
   using ccInf_lower [of "f ` A"] by simp
 
-lemma ccINF_greatest: "countable A \<Longrightarrow> (\<And>i. i \<in> A \<Longrightarrow> u \<le> f i) \<Longrightarrow> u \<le> (INF i :A. f i)"
+lemma ccINF_greatest: "countable A \<Longrightarrow> (\<And>i. i \<in> A \<Longrightarrow> u \<le> f i) \<Longrightarrow> u \<le> (INF i \<in> A. f i)"
   using ccInf_greatest [of "f ` A"] by auto
 
-lemma ccSUP_upper: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> f i \<le> (SUP i :A. f i)"
+lemma ccSUP_upper: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> f i \<le> (SUP i \<in> A. f i)"
   using ccSup_upper [of "f ` A"] by simp
 
-lemma ccSUP_least: "countable A \<Longrightarrow> (\<And>i. i \<in> A \<Longrightarrow> f i \<le> u) \<Longrightarrow> (SUP i :A. f i) \<le> u"
+lemma ccSUP_least: "countable A \<Longrightarrow> (\<And>i. i \<in> A \<Longrightarrow> f i \<le> u) \<Longrightarrow> (SUP i \<in> A. f i) \<le> u"
   using ccSup_least [of "f ` A"] by auto
 
 lemma ccInf_lower2: "countable A \<Longrightarrow> u \<in> A \<Longrightarrow> u \<le> v \<Longrightarrow> Inf A \<le> v"
   using ccInf_lower [of A u] by auto
 
-lemma ccINF_lower2: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> f i \<le> u \<Longrightarrow> (INF i :A. f i) \<le> u"
+lemma ccINF_lower2: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> f i \<le> u \<Longrightarrow> (INF i \<in> A. f i) \<le> u"
   using ccINF_lower [of A i f] by auto
 
 lemma ccSup_upper2: "countable A \<Longrightarrow> u \<in> A \<Longrightarrow> v \<le> u \<Longrightarrow> v \<le> Sup A"
   using ccSup_upper [of A u] by auto
 
-lemma ccSUP_upper2: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> u \<le> f i \<Longrightarrow> u \<le> (SUP i :A. f i)"
+lemma ccSUP_upper2: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> u \<le> f i \<Longrightarrow> u \<le> (SUP i \<in> A. f i)"
   using ccSUP_upper [of A i f] by auto
 
 lemma le_ccInf_iff: "countable A \<Longrightarrow> b \<le> Inf A \<longleftrightarrow> (\<forall>a\<in>A. b \<le> a)"
   by (auto intro: ccInf_greatest dest: ccInf_lower)
 
-lemma le_ccINF_iff: "countable A \<Longrightarrow> u \<le> (INF i :A. f i) \<longleftrightarrow> (\<forall>i\<in>A. u \<le> f i)"
+lemma le_ccINF_iff: "countable A \<Longrightarrow> u \<le> (INF i \<in> A. f i) \<longleftrightarrow> (\<forall>i\<in>A. u \<le> f i)"
   using le_ccInf_iff [of "f ` A"] by simp
 
 lemma ccSup_le_iff: "countable A \<Longrightarrow> Sup A \<le> b \<longleftrightarrow> (\<forall>a\<in>A. a \<le> b)"
   by (auto intro: ccSup_least dest: ccSup_upper)
 
-lemma ccSUP_le_iff: "countable A \<Longrightarrow> (SUP i :A. f i) \<le> u \<longleftrightarrow> (\<forall>i\<in>A. f i \<le> u)"
+lemma ccSUP_le_iff: "countable A \<Longrightarrow> (SUP i \<in> A. f i) \<le> u \<longleftrightarrow> (\<forall>i\<in>A. f i \<le> u)"
   using ccSup_le_iff [of "f ` A"] by simp
 
 lemma ccInf_insert [simp]: "countable A \<Longrightarrow> Inf (insert a A) = inf a (Inf A)"
   by (force intro: le_infI le_infI1 le_infI2 antisym ccInf_greatest ccInf_lower)
 
-lemma ccINF_insert [simp]: "countable A \<Longrightarrow> (INF x:insert a A. f x) = inf (f a) (INFIMUM A f)"
+lemma ccINF_insert [simp]: "countable A \<Longrightarrow> (INF x\<in>insert a A. f x) = inf (f a) (INFIMUM A f)"
   unfolding image_insert by simp
 
 lemma ccSup_insert [simp]: "countable A \<Longrightarrow> Sup (insert a A) = sup a (Sup A)"
   by (force intro: le_supI le_supI1 le_supI2 antisym ccSup_least ccSup_upper)
 
-lemma ccSUP_insert [simp]: "countable A \<Longrightarrow> (SUP x:insert a A. f x) = sup (f a) (SUPREMUM A f)"
+lemma ccSUP_insert [simp]: "countable A \<Longrightarrow> (SUP x\<in>insert a A. f x) = sup (f a) (SUPREMUM A f)"
   unfolding image_insert by simp
 
-lemma ccINF_empty [simp]: "(INF x:{}. f x) = top"
+lemma ccINF_empty [simp]: "(INF x\<in>{}. f x) = top"
   unfolding image_empty by simp
 
-lemma ccSUP_empty [simp]: "(SUP x:{}. f x) = bot"
+lemma ccSUP_empty [simp]: "(SUP x\<in>{}. f x) = bot"
   unfolding image_empty by simp
 
 lemma ccInf_superset_mono: "countable A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> Inf A \<le> Inf B"
@@ -99,7 +99,7 @@
 qed auto
 
 lemma ccINF_mono:
-  "countable A \<Longrightarrow> countable B \<Longrightarrow> (\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<le> g m) \<Longrightarrow> (INF n:A. f n) \<le> (INF n:B. g n)"
+  "countable A \<Longrightarrow> countable B \<Longrightarrow> (\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<le> g m) \<Longrightarrow> (INF n\<in>A. f n) \<le> (INF n\<in>B. g n)"
   using ccInf_mono [of "g ` B" "f ` A"] by auto
 
 lemma ccSup_mono:
@@ -114,15 +114,15 @@
 qed auto
 
 lemma ccSUP_mono:
-  "countable A \<Longrightarrow> countable B \<Longrightarrow> (\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<le> g m) \<Longrightarrow> (SUP n:A. f n) \<le> (SUP n:B. g n)"
+  "countable A \<Longrightarrow> countable B \<Longrightarrow> (\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<le> g m) \<Longrightarrow> (SUP n\<in>A. f n) \<le> (SUP n\<in>B. g n)"
   using ccSup_mono [of "g ` B" "f ` A"] by auto
 
 lemma ccINF_superset_mono:
-  "countable A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (INF x:A. f x) \<le> (INF x:B. g x)"
+  "countable A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (INF x\<in>A. f x) \<le> (INF x\<in>B. g x)"
   by (blast intro: ccINF_mono countable_subset dest: subsetD)
 
 lemma ccSUP_subset_mono:
-  "countable B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (SUP x:A. f x) \<le> (SUP x:B. g x)"
+  "countable B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (SUP x\<in>A. f x) \<le> (SUP x\<in>B. g x)"
   by (blast intro: ccSUP_mono countable_subset dest: subsetD)
 
 
@@ -136,38 +136,38 @@
   by (rule antisym) (auto intro: ccInf_greatest ccInf_lower le_infI1 le_infI2)
 
 lemma ccINF_union:
-  "countable A \<Longrightarrow> countable B \<Longrightarrow> (INF i:A \<union> B. M i) = inf (INF i:A. M i) (INF i:B. M i)"
+  "countable A \<Longrightarrow> countable B \<Longrightarrow> (INF i\<in>A \<union> B. M i) = inf (INF i\<in>A. M i) (INF i\<in>B. M i)"
   by (auto intro!: antisym ccINF_mono intro: le_infI1 le_infI2 ccINF_greatest ccINF_lower)
 
 lemma ccSup_union_distrib: "countable A \<Longrightarrow> countable B \<Longrightarrow> Sup (A \<union> B) = sup (Sup A) (Sup B)"
   by (rule antisym) (auto intro: ccSup_least ccSup_upper le_supI1 le_supI2)
 
 lemma ccSUP_union:
-  "countable A \<Longrightarrow> countable B \<Longrightarrow> (SUP i:A \<union> B. M i) = sup (SUP i:A. M i) (SUP i:B. M i)"
+  "countable A \<Longrightarrow> countable B \<Longrightarrow> (SUP i\<in>A \<union> B. M i) = sup (SUP i\<in>A. M i) (SUP i\<in>B. M i)"
   by (auto intro!: antisym ccSUP_mono intro: le_supI1 le_supI2 ccSUP_least ccSUP_upper)
 
-lemma ccINF_inf_distrib: "countable A \<Longrightarrow> inf (INF a:A. f a) (INF a:A. g a) = (INF a:A. inf (f a) (g a))"
+lemma ccINF_inf_distrib: "countable A \<Longrightarrow> inf (INF a\<in>A. f a) (INF a\<in>A. g a) = (INF a\<in>A. inf (f a) (g a))"
   by (rule antisym) (rule ccINF_greatest, auto intro: le_infI1 le_infI2 ccINF_lower ccINF_mono)
 
-lemma ccSUP_sup_distrib: "countable A \<Longrightarrow> sup (SUP a:A. f a) (SUP a:A. g a) = (SUP a:A. sup (f a) (g a))"
+lemma ccSUP_sup_distrib: "countable A \<Longrightarrow> sup (SUP a\<in>A. f a) (SUP a\<in>A. g a) = (SUP a\<in>A. sup (f a) (g a))"
   by (rule antisym[rotated]) (rule ccSUP_least, auto intro: le_supI1 le_supI2 ccSUP_upper ccSUP_mono)
 
-lemma ccINF_const [simp]: "A \<noteq> {} \<Longrightarrow> (INF i :A. f) = f"
+lemma ccINF_const [simp]: "A \<noteq> {} \<Longrightarrow> (INF i \<in> A. f) = f"
   unfolding image_constant_conv by auto
 
-lemma ccSUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (SUP i :A. f) = f"
+lemma ccSUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (SUP i \<in> A. f) = f"
   unfolding image_constant_conv by auto
 
-lemma ccINF_top [simp]: "(INF x:A. top) = top"
+lemma ccINF_top [simp]: "(INF x\<in>A. top) = top"
   by (cases "A = {}") simp_all
 
-lemma ccSUP_bot [simp]: "(SUP x:A. bot) = bot"
+lemma ccSUP_bot [simp]: "(SUP x\<in>A. bot) = bot"
   by (cases "A = {}") simp_all
 
-lemma ccINF_commute: "countable A \<Longrightarrow> countable B \<Longrightarrow> (INF i:A. INF j:B. f i j) = (INF j:B. INF i:A. f i j)"
+lemma ccINF_commute: "countable A \<Longrightarrow> countable B \<Longrightarrow> (INF i\<in>A. INF j\<in>B. f i j) = (INF j\<in>B. INF i\<in>A. f i j)"
   by (iprover intro: ccINF_lower ccINF_greatest order_trans antisym)
 
-lemma ccSUP_commute: "countable A \<Longrightarrow> countable B \<Longrightarrow> (SUP i:A. SUP j:B. f i j) = (SUP j:B. SUP i:A. f i j)"
+lemma ccSUP_commute: "countable A \<Longrightarrow> countable B \<Longrightarrow> (SUP i\<in>A. SUP j\<in>B. f i j) = (SUP j\<in>B. SUP i\<in>A. f i j)"
   by (iprover intro: ccSUP_upper ccSUP_least order_trans antisym)
 
 end
@@ -179,61 +179,61 @@
 lemma less_ccSup_iff: "countable S \<Longrightarrow> a < Sup S \<longleftrightarrow> (\<exists>x\<in>S. a < x)"
   unfolding not_le [symmetric] by (subst ccSup_le_iff) auto
 
-lemma less_ccSUP_iff: "countable A \<Longrightarrow> a < (SUP i:A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a < f x)"
+lemma less_ccSUP_iff: "countable A \<Longrightarrow> a < (SUP i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a < f x)"
   using less_ccSup_iff [of "f ` A"] by simp
 
 lemma ccInf_less_iff: "countable S \<Longrightarrow> Inf S < a \<longleftrightarrow> (\<exists>x\<in>S. x < a)"
   unfolding not_le [symmetric] by (subst le_ccInf_iff) auto
 
-lemma ccINF_less_iff: "countable A \<Longrightarrow> (INF i:A. f i) < a \<longleftrightarrow> (\<exists>x\<in>A. f x < a)"
+lemma ccINF_less_iff: "countable A \<Longrightarrow> (INF i\<in>A. f i) < a \<longleftrightarrow> (\<exists>x\<in>A. f x < a)"
   using ccInf_less_iff [of "f ` A"] by simp
 
 end
 
 class countable_complete_distrib_lattice = countable_complete_lattice +
-  assumes sup_ccInf: "countable B \<Longrightarrow> sup a (Inf B) = (INF b:B. sup a b)"
-  assumes inf_ccSup: "countable B \<Longrightarrow> inf a (Sup B) = (SUP b:B. inf a b)"
+  assumes sup_ccInf: "countable B \<Longrightarrow> sup a (Inf B) = (INF b\<in>B. sup a b)"
+  assumes inf_ccSup: "countable B \<Longrightarrow> inf a (Sup B) = (SUP b\<in>B. inf a b)"
 begin
 
 lemma sup_ccINF:
-  "countable B \<Longrightarrow> sup a (INF b:B. f b) = (INF b:B. sup a (f b))"
+  "countable B \<Longrightarrow> sup a (INF b\<in>B. f b) = (INF b\<in>B. sup a (f b))"
   by (simp only: sup_ccInf image_image countable_image)
 
 lemma inf_ccSUP:
-  "countable B \<Longrightarrow> inf a (SUP b:B. f b) = (SUP b:B. inf a (f b))"
+  "countable B \<Longrightarrow> inf a (SUP b\<in>B. f b) = (SUP b\<in>B. inf a (f b))"
   by (simp only: inf_ccSup image_image countable_image)
 
 subclass distrib_lattice
 proof
   fix a b c
-  from sup_ccInf[of "{b, c}" a] have "sup a (Inf {b, c}) = (INF d:{b, c}. sup a d)"
+  from sup_ccInf[of "{b, c}" a] have "sup a (Inf {b, c}) = (INF d\<in>{b, c}. sup a d)"
     by simp
   then show "sup a (inf b c) = inf (sup a b) (sup a c)"
     by simp
 qed
 
 lemma ccInf_sup:
-  "countable B \<Longrightarrow> sup (Inf B) a = (INF b:B. sup b a)"
+  "countable B \<Longrightarrow> sup (Inf B) a = (INF b\<in>B. sup b a)"
   by (simp add: sup_ccInf sup_commute)
 
 lemma ccSup_inf:
-  "countable B \<Longrightarrow> inf (Sup B) a = (SUP b:B. inf b a)"
+  "countable B \<Longrightarrow> inf (Sup B) a = (SUP b\<in>B. inf b a)"
   by (simp add: inf_ccSup inf_commute)
 
 lemma ccINF_sup:
-  "countable B \<Longrightarrow> sup (INF b:B. f b) a = (INF b:B. sup (f b) a)"
+  "countable B \<Longrightarrow> sup (INF b\<in>B. f b) a = (INF b\<in>B. sup (f b) a)"
   by (simp add: sup_ccINF sup_commute)
 
 lemma ccSUP_inf:
-  "countable B \<Longrightarrow> inf (SUP b:B. f b) a = (SUP b:B. inf (f b) a)"
+  "countable B \<Longrightarrow> inf (SUP b\<in>B. f b) a = (SUP b\<in>B. inf (f b) a)"
   by (simp add: inf_ccSUP inf_commute)
 
 lemma ccINF_sup_distrib2:
-  "countable A \<Longrightarrow> countable B \<Longrightarrow> sup (INF a:A. f a) (INF b:B. g b) = (INF a:A. INF b:B. sup (f a) (g b))"
+  "countable A \<Longrightarrow> countable B \<Longrightarrow> sup (INF a\<in>A. f a) (INF b\<in>B. g b) = (INF a\<in>A. INF b\<in>B. sup (f a) (g b))"
   by (subst ccINF_commute) (simp_all add: sup_ccINF ccINF_sup)
 
 lemma ccSUP_inf_distrib2:
-  "countable A \<Longrightarrow> countable B \<Longrightarrow> inf (SUP a:A. f a) (SUP b:B. g b) = (SUP a:A. SUP b:B. inf (f a) (g b))"
+  "countable A \<Longrightarrow> countable B \<Longrightarrow> inf (SUP a\<in>A. f a) (SUP b\<in>B. g b) = (SUP a\<in>A. SUP b\<in>B. inf (f a) (g b))"
   by (subst ccSUP_commute) (simp_all add: inf_ccSUP ccSUP_inf)
 
 context
@@ -242,20 +242,20 @@
 begin
 
 lemma mono_ccInf:
-  "countable A \<Longrightarrow> f (Inf A) \<le> (INF x:A. f x)"
+  "countable A \<Longrightarrow> f (Inf A) \<le> (INF x\<in>A. f x)"
   using \<open>mono f\<close>
   by (auto intro!: countable_complete_lattice_class.ccINF_greatest intro: ccInf_lower dest: monoD)
 
 lemma mono_ccSup:
-  "countable A \<Longrightarrow> (SUP x:A. f x) \<le> f (Sup A)"
+  "countable A \<Longrightarrow> (SUP x\<in>A. f x) \<le> f (Sup A)"
   using \<open>mono f\<close> by (auto intro: countable_complete_lattice_class.ccSUP_least ccSup_upper dest: monoD)
 
 lemma mono_ccINF:
-  "countable I \<Longrightarrow> f (INF i : I. A i) \<le> (INF x : I. f (A x))"
+  "countable I \<Longrightarrow> f (INF i \<in> I. A i) \<le> (INF x \<in> I. f (A x))"
   by (intro countable_complete_lattice_class.ccINF_greatest monoD[OF \<open>mono f\<close>] ccINF_lower)
 
 lemma mono_ccSUP:
-  "countable I \<Longrightarrow> (SUP x : I. f (A x)) \<le> f (SUP i : I. A i)"
+  "countable I \<Longrightarrow> (SUP x \<in> I. f (A x)) \<le> f (SUP i \<in> I. A i)"
   by (intro countable_complete_lattice_class.ccSUP_least monoD[OF \<open>mono f\<close>] ccSUP_upper)
 
 end
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Library/Extended_Nonnegative_Real.thy
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -108,12 +108,12 @@
 lemma sup_continuous_SUP[order_continuous_intros]:
   fixes M :: "_ \<Rightarrow> _ \<Rightarrow> 'a::complete_lattice"
   assumes M: "\<And>i. i \<in> I \<Longrightarrow> sup_continuous (M i)"
-  shows  "sup_continuous (SUP i:I. M i)"
+  shows  "sup_continuous (SUP i\<in>I. M i)"
   unfolding sup_continuous_def by (auto simp add: sup_continuousD[OF M] intro: SUP_commute)
 
 lemma sup_continuous_apply_SUP[order_continuous_intros]:
   fixes M :: "_ \<Rightarrow> _ \<Rightarrow> 'a::complete_lattice"
-  shows "(\<And>i. i \<in> I \<Longrightarrow> sup_continuous (M i)) \<Longrightarrow> sup_continuous (\<lambda>x. SUP i:I. M i x)"
+  shows "(\<And>i. i \<in> I \<Longrightarrow> sup_continuous (M i)) \<Longrightarrow> sup_continuous (\<lambda>x. SUP i\<in>I. M i x)"
   unfolding SUP_apply[symmetric] by (rule sup_continuous_SUP)
 
 lemma sup_continuous_lfp'[order_continuous_intros]:
@@ -145,7 +145,7 @@
 qed
 
 lemma mono_INF_fun:
-    "(\<And>x y. mono (F x y)) \<Longrightarrow> mono (\<lambda>z x. INF y : X x. F x y z :: 'a :: complete_lattice)"
+    "(\<And>x y. mono (F x y)) \<Longrightarrow> mono (\<lambda>z x. INF y \<in> X x. F x y z :: 'a :: complete_lattice)"
   by (auto intro!: INF_mono[OF bexI] simp: le_fun_def mono_def)
 
 lemma continuous_on_max:
@@ -160,22 +160,22 @@
 
 lemma real_of_nat_Sup:
   assumes "A \<noteq> {}" "bdd_above A"
-  shows "of_nat (Sup A) = (SUP a:A. of_nat a :: real)"
+  shows "of_nat (Sup A) = (SUP a\<in>A. of_nat a :: real)"
 proof (intro antisym)
-  show "(SUP a:A. of_nat a::real) \<le> of_nat (Sup A)"
+  show "(SUP a\<in>A. of_nat a::real) \<le> of_nat (Sup A)"
     using assms by (intro cSUP_least of_nat_mono) (auto intro: cSup_upper)
   have "Sup A \<in> A"
     unfolding Sup_nat_def using assms by (intro Max_in) (auto simp: bdd_above_nat)
-  then show "of_nat (Sup A) \<le> (SUP a:A. of_nat a::real)"
+  then show "of_nat (Sup A) \<le> (SUP a\<in>A. of_nat a::real)"
     by (intro cSUP_upper bdd_above_image_mono assms) (auto simp: mono_def)
 qed
 
 lemma (in complete_lattice) SUP_sup_const1:
-  "I \<noteq> {} \<Longrightarrow> (SUP i:I. sup c (f i)) = sup c (SUP i:I. f i)"
+  "I \<noteq> {} \<Longrightarrow> (SUP i\<in>I. sup c (f i)) = sup c (SUP i\<in>I. f i)"
   using SUP_sup_distrib[of "\<lambda>_. c" I f] by simp
 
 lemma (in complete_lattice) SUP_sup_const2:
-  "I \<noteq> {} \<Longrightarrow> (SUP i:I. sup (f i) c) = sup (SUP i:I. f i) c"
+  "I \<noteq> {} \<Longrightarrow> (SUP i\<in>I. sup (f i) c) = sup (SUP i\<in>I. f i) c"
   using SUP_sup_distrib[of f I "\<lambda>_. c"] by simp
 
 lemma one_less_of_natD:
@@ -350,7 +350,7 @@
 
 lemma rel_fun_limsup[transfer_rule]: "rel_fun (rel_fun (=) pcr_ennreal) pcr_ennreal limsup limsup"
 proof -
-  have "rel_fun (rel_fun (=) pcr_ennreal) pcr_ennreal (\<lambda>x. INF n. sup 0 (SUP i:{n..}. x i)) limsup"
+  have "rel_fun (rel_fun (=) pcr_ennreal) pcr_ennreal (\<lambda>x. INF n. sup 0 (SUP i\<in>{n..}. x i)) limsup"
     unfolding limsup_INF_SUP[abs_def] by (transfer_prover_start, transfer_step+; simp)
   then show ?thesis
     unfolding limsup_INF_SUP[abs_def]
@@ -1140,13 +1140,13 @@
 lemma of_nat_less_ennreal_of_nat[simp]: "of_nat n \<le> ennreal_of_enat x \<longleftrightarrow> of_nat n \<le> x"
   by (cases x) (auto simp: of_nat_eq_enat)
 
-lemma ennreal_of_enat_Sup: "ennreal_of_enat (Sup X) = (SUP x:X. ennreal_of_enat x)"
+lemma ennreal_of_enat_Sup: "ennreal_of_enat (Sup X) = (SUP x\<in>X. ennreal_of_enat x)"
 proof -
-  have "ennreal_of_enat (Sup X) \<le> (SUP x : X. ennreal_of_enat x)"
+  have "ennreal_of_enat (Sup X) \<le> (SUP x \<in> X. ennreal_of_enat x)"
     unfolding Sup_enat_def
   proof (clarsimp, intro conjI impI)
     fix x assume "finite X" "X \<noteq> {}"
-    then show "ennreal_of_enat (Max X) \<le> (SUP x : X. ennreal_of_enat x)"
+    then show "ennreal_of_enat (Max X) \<le> (SUP x \<in> X. ennreal_of_enat x)"
       by (intro SUP_upper Max_in)
   next
     assume "infinite X" "X \<noteq> {}"
@@ -1162,9 +1162,9 @@
       with x show ?thesis
         by (auto intro!: bexI[of _ x] less_le_trans[OF n])
     qed
-    then have "(SUP x : X. ennreal_of_enat x) = top"
+    then have "(SUP x \<in> X. ennreal_of_enat x) = top"
       by simp
-    then show "top \<le> (SUP x : X. ennreal_of_enat x)"
+    then show "top \<le> (SUP x \<in> X. ennreal_of_enat x)"
       unfolding top_unique by simp
   qed
   then show ?thesis
@@ -1395,7 +1395,7 @@
 lemma ennreal_suminf_SUP_eq_directed:
   fixes f :: "'a \<Rightarrow> nat \<Rightarrow> ennreal"
   assumes *: "\<And>N i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> finite N \<Longrightarrow> \<exists>k\<in>I. \<forall>n\<in>N. f i n \<le> f k n \<and> f j n \<le> f k n"
-  shows "(\<Sum>n. SUP i:I. f i n) = (SUP i:I. \<Sum>n. f i n)"
+  shows "(\<Sum>n. SUP i\<in>I. f i n) = (SUP i\<in>I. \<Sum>n. f i n)"
 proof cases
   assume "I \<noteq> {}"
   then obtain i where "i \<in> I" by auto
@@ -1417,16 +1417,16 @@
   shows "(INF i. c + f i) = c + (INF i. f i)"
   using INF_ennreal_add_const[of f c] by (simp add: ac_simps)
 
-lemma SUP_mult_left_ennreal: "c * (SUP i:I. f i) = (SUP i:I. c * f i ::ennreal)"
+lemma SUP_mult_left_ennreal: "c * (SUP i\<in>I. f i) = (SUP i\<in>I. c * f i ::ennreal)"
 proof cases
   assume "I \<noteq> {}" then show ?thesis
     by transfer (auto simp add: SUP_ereal_mult_left max_absorb2 SUP_upper2)
 qed (simp add: bot_ennreal)
 
-lemma SUP_mult_right_ennreal: "(SUP i:I. f i) * c = (SUP i:I. f i * c ::ennreal)"
+lemma SUP_mult_right_ennreal: "(SUP i\<in>I. f i) * c = (SUP i\<in>I. f i * c ::ennreal)"
   using SUP_mult_left_ennreal by (simp add: mult.commute)
 
-lemma SUP_divide_ennreal: "(SUP i:I. f i) / c = (SUP i:I. f i / c ::ennreal)"
+lemma SUP_divide_ennreal: "(SUP i\<in>I. f i) / c = (SUP i\<in>I. f i / c ::ennreal)"
   using SUP_mult_right_ennreal by (simp add: divide_ennreal_def)
 
 lemma ennreal_SUP_of_nat_eq_top: "(SUP x. of_nat x :: ennreal) = top"
@@ -1442,9 +1442,9 @@
 lemma ennreal_SUP_eq_top:
   fixes f :: "'a \<Rightarrow> ennreal"
   assumes "\<And>n. \<exists>i\<in>I. of_nat n \<le> f i"
-  shows "(SUP i : I. f i) = top"
+  shows "(SUP i \<in> I. f i) = top"
 proof -
-  have "(SUP x. of_nat x :: ennreal) \<le> (SUP i : I. f i)"
+  have "(SUP x. of_nat x :: ennreal) \<le> (SUP i \<in> I. f i)"
     using assms by (auto intro!: SUP_least intro: SUP_upper2)
   then show ?thesis
     by (auto simp: ennreal_SUP_of_nat_eq_top top_unique)
@@ -1452,19 +1452,19 @@
 
 lemma ennreal_INF_const_minus:
   fixes f :: "'a \<Rightarrow> ennreal"
-  shows "I \<noteq> {} \<Longrightarrow> (SUP x:I. c - f x) = c - (INF x:I. f x)"
+  shows "I \<noteq> {} \<Longrightarrow> (SUP x\<in>I. c - f x) = c - (INF x\<in>I. f x)"
   by (transfer fixing: I)
      (simp add: sup_max[symmetric] SUP_sup_const1 SUP_ereal_minus_right del: sup_ereal_def)
 
 lemma of_nat_Sup_ennreal:
   assumes "A \<noteq> {}" "bdd_above A"
-  shows "of_nat (Sup A) = (SUP a:A. of_nat a :: ennreal)"
+  shows "of_nat (Sup A) = (SUP a\<in>A. of_nat a :: ennreal)"
 proof (intro antisym)
-  show "(SUP a:A. of_nat a::ennreal) \<le> of_nat (Sup A)"
+  show "(SUP a\<in>A. of_nat a::ennreal) \<le> of_nat (Sup A)"
     by (intro SUP_least of_nat_mono) (auto intro: cSup_upper assms)
   have "Sup A \<in> A"
     unfolding Sup_nat_def using assms by (intro Max_in) (auto simp: bdd_above_nat)
-  then show "of_nat (Sup A) \<le> (SUP a:A. of_nat a::ennreal)"
+  then show "of_nat (Sup A) \<le> (SUP a\<in>A. of_nat a::ennreal)"
     by (intro SUP_upper)
 qed
 
@@ -1601,18 +1601,18 @@
 lemma SUP_sup_continuous_ennreal:
   fixes f :: "ennreal \<Rightarrow> 'a::complete_lattice"
   assumes f: "sup_continuous f" and "I \<noteq> {}"
-  shows "(SUP i:I. f (g i)) = f (SUP i:I. g i)"
+  shows "(SUP i\<in>I. f (g i)) = f (SUP i\<in>I. g i)"
 proof (rule antisym)
-  show "(SUP i:I. f (g i)) \<le> f (SUP i:I. g i)"
+  show "(SUP i\<in>I. f (g i)) \<le> f (SUP i\<in>I. g i)"
     by (rule mono_SUP[OF sup_continuous_mono[OF f]])
   from ennreal_Sup_countable_SUP[of "g`I"] \<open>I \<noteq> {}\<close>
-  obtain M :: "nat \<Rightarrow> ennreal" where "incseq M" and M: "range M \<subseteq> g ` I" and eq: "(SUP i : I. g i) = (SUP i. M i)"
+  obtain M :: "nat \<Rightarrow> ennreal" where "incseq M" and M: "range M \<subseteq> g ` I" and eq: "(SUP i \<in> I. g i) = (SUP i. M i)"
     by auto
-  have "f (SUP i : I. g i) = (SUP i : range M. f i)"
+  have "f (SUP i \<in> I. g i) = (SUP i \<in> range M. f i)"
     unfolding eq sup_continuousD[OF f \<open>mono M\<close>] by simp
-  also have "\<dots> \<le> (SUP i : I. f (g i))"
+  also have "\<dots> \<le> (SUP i \<in> I. f (g i))"
     by (insert M, drule SUP_subset_mono) auto
-  finally show "f (SUP i : I. g i) \<le> (SUP i : I. f (g i))" .
+  finally show "f (SUP i \<in> I. g i) \<le> (SUP i \<in> I. f (g i))" .
 qed
 
 lemma ennreal_suminf_SUP_eq:
@@ -1625,7 +1625,7 @@
 
 lemma ennreal_SUP_add_left:
   fixes c :: ennreal
-  shows "I \<noteq> {} \<Longrightarrow> (SUP i:I. f i + c) = (SUP i:I. f i) + c"
+  shows "I \<noteq> {} \<Longrightarrow> (SUP i\<in>I. f i + c) = (SUP i\<in>I. f i) + c"
   apply transfer
   apply (simp add: SUP_ereal_add_left)
   apply (subst (1 2) max.absorb2)
@@ -1634,7 +1634,7 @@
 
 lemma ennreal_SUP_const_minus: (* TODO: rename: ennreal_SUP_const_minus *)
   fixes f :: "'a \<Rightarrow> ennreal"
-  shows "I \<noteq> {} \<Longrightarrow> c < top \<Longrightarrow> (INF x:I. c - f x) = c - (SUP x:I. f x)"
+  shows "I \<noteq> {} \<Longrightarrow> c < top \<Longrightarrow> (INF x\<in>I. c - f x) = c - (SUP x\<in>I. f x)"
   apply (transfer fixing: I)
   unfolding ex_in_conv[symmetric]
   apply (auto simp add: sup_max[symmetric] SUP_upper2 sup_absorb2
@@ -1648,11 +1648,11 @@
 lemma INF_approx_ennreal:
   fixes x::ennreal and e::real
   assumes "e > 0"
-  assumes INF: "x = (INF i : A. f i)"
+  assumes INF: "x = (INF i \<in> A. f i)"
   assumes "x \<noteq> \<infinity>"
   shows "\<exists>i \<in> A. f i < x + e"
 proof -
-  have "(INF i : A. f i) < x + e"
+  have "(INF i \<in> A. f i) < x + e"
     unfolding INF[symmetric] using \<open>0<e\<close> \<open>x \<noteq> \<infinity>\<close> by (cases x) auto
   then show ?thesis
     unfolding INF_less_iff .
@@ -1661,13 +1661,13 @@
 lemma SUP_approx_ennreal:
   fixes x::ennreal and e::real
   assumes "e > 0" "A \<noteq> {}"
-  assumes SUP: "x = (SUP i : A. f i)"
+  assumes SUP: "x = (SUP i \<in> A. f i)"
   assumes "x \<noteq> \<infinity>"
   shows "\<exists>i \<in> A. x < f i + e"
 proof -
   have "x < x + e"
     using \<open>0<e\<close> \<open>x \<noteq> \<infinity>\<close> by (cases x) auto
-  also have "x + e = (SUP i : A. f i + e)"
+  also have "x + e = (SUP i \<in> A. f i + e)"
     unfolding SUP ennreal_SUP_add_left[OF \<open>A \<noteq> {}\<close>] ..
   finally show ?thesis
     unfolding less_SUP_iff .
@@ -1677,17 +1677,17 @@
   fixes x::ennreal
   assumes f_bound: "\<And>i. i \<in> A \<Longrightarrow> f i \<le> x"
   assumes approx: "\<And>e. (e::real) > 0 \<Longrightarrow> \<exists>i \<in> A. x \<le> f i + e"
-  shows "x = (SUP i : A. f i)"
+  shows "x = (SUP i \<in> A. f i)"
 proof (rule antisym)
-  show "x \<le> (SUP i:A. f i)"
+  show "x \<le> (SUP i\<in>A. f i)"
   proof (rule ennreal_le_epsilon)
     fix e :: real assume "0 < e"
     from approx[OF this] guess i ..
     then have "x \<le> f i + e"
       by simp
-    also have "\<dots> \<le> (SUP i:A. f i) + e"
+    also have "\<dots> \<le> (SUP i\<in>A. f i) + e"
       by (intro add_mono \<open>i \<in> A\<close> SUP_upper order_refl)
-    finally show "x \<le> (SUP i:A. f i) + e" .
+    finally show "x \<le> (SUP i\<in>A. f i) + e" .
   qed
 qed (intro SUP_least f_bound)
 
@@ -1695,17 +1695,17 @@
   fixes x::ennreal
   assumes f_bound: "\<And>i. i \<in> A \<Longrightarrow> x \<le> f i"
   assumes approx: "\<And>e. (e::real) > 0 \<Longrightarrow> \<exists>i \<in> A. f i \<le> x + e"
-  shows "x = (INF i : A. f i)"
+  shows "x = (INF i \<in> A. f i)"
 proof (rule antisym)
-  show "(INF i:A. f i) \<le> x"
+  show "(INF i\<in>A. f i) \<le> x"
   proof (rule ennreal_le_epsilon)
     fix e :: real assume "0 < e"
     from approx[OF this] guess i .. note i = this
-    then have "(INF i:A. f i) \<le> f i"
+    then have "(INF i\<in>A. f i) \<le> f i"
       by (intro INF_lower)
     also have "\<dots> \<le> x + e"
       by fact
-    finally show "(INF i:A. f i) \<le> x + e" .
+    finally show "(INF i\<in>A. f i) \<le> x + e" .
   qed
 qed (intro INF_greatest f_bound)
 
@@ -1786,7 +1786,7 @@
   by (cases "0 \<le> x") (auto simp: ennreal_neg ennreal_less_iff simp flip: ennreal_1)
 
 lemma SUP_const_minus_ennreal:
-  fixes f :: "'a \<Rightarrow> ennreal" shows "I \<noteq> {} \<Longrightarrow> (SUP x:I. c - f x) = c - (INF x:I. f x)"
+  fixes f :: "'a \<Rightarrow> ennreal" shows "I \<noteq> {} \<Longrightarrow> (SUP x\<in>I. c - f x) = c - (INF x\<in>I. f x)"
   including ennreal.lifting
   by (transfer fixing: I)
      (simp add: SUP_sup_distrib[symmetric] SUP_ereal_minus_right
@@ -1929,18 +1929,18 @@
   done
 
 lemma SUP_diff_ennreal:
-  "c < top \<Longrightarrow> (SUP i:I. f i - c :: ennreal) = (SUP i:I. f i) - c"
+  "c < top \<Longrightarrow> (SUP i\<in>I. f i - c :: ennreal) = (SUP i\<in>I. f i) - c"
   by (auto intro!: SUP_eqI ennreal_minus_mono SUP_least intro: SUP_upper
            simp: ennreal_minus_cancel_iff ennreal_minus_le_iff less_top[symmetric])
 
 lemma ennreal_SUP_add_right:
-  fixes c :: ennreal shows "I \<noteq> {} \<Longrightarrow> c + (SUP i:I. f i) = (SUP i:I. c + f i)"
+  fixes c :: ennreal shows "I \<noteq> {} \<Longrightarrow> c + (SUP i\<in>I. f i) = (SUP i\<in>I. c + f i)"
   using ennreal_SUP_add_left[of I f c] by (simp add: add.commute)
 
 lemma SUP_add_directed_ennreal:
   fixes f g :: "_ \<Rightarrow> ennreal"
   assumes directed: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> \<exists>k\<in>I. f i + g j \<le> f k + g k"
-  shows "(SUP i:I. f i + g i) = (SUP i:I. f i) + (SUP i:I. g i)"
+  shows "(SUP i\<in>I. f i + g i) = (SUP i\<in>I. f i) + (SUP i\<in>I. g i)"
 proof cases
   assume "I = {}" then show ?thesis
     by (simp add: bot_ereal_def)
@@ -1948,16 +1948,16 @@
   assume "I \<noteq> {}"
   show ?thesis
   proof (rule antisym)
-    show "(SUP i:I. f i + g i) \<le> (SUP i:I. f i) + (SUP i:I. g i)"
+    show "(SUP i\<in>I. f i + g i) \<le> (SUP i\<in>I. f i) + (SUP i\<in>I. g i)"
       by (rule SUP_least; intro add_mono SUP_upper)
   next
-    have "(SUP i:I. f i) + (SUP i:I. g i) = (SUP i:I. f i + (SUP i:I. g i))"
+    have "(SUP i\<in>I. f i) + (SUP i\<in>I. g i) = (SUP i\<in>I. f i + (SUP i\<in>I. g i))"
       by (intro ennreal_SUP_add_left[symmetric] \<open>I \<noteq> {}\<close>)
-    also have "\<dots> = (SUP i:I. (SUP j:I. f i + g j))"
+    also have "\<dots> = (SUP i\<in>I. (SUP j\<in>I. f i + g j))"
       by (intro SUP_cong refl ennreal_SUP_add_right \<open>I \<noteq> {}\<close>)
-    also have "\<dots> \<le> (SUP i:I. f i + g i)"
+    also have "\<dots> \<le> (SUP i\<in>I. f i + g i)"
       using directed by (intro SUP_least) (blast intro: SUP_upper2)
-    finally show "(SUP i:I. f i) + (SUP i:I. g i) \<le> (SUP i:I. f i + g i)" .
+    finally show "(SUP i\<in>I. f i) + (SUP i\<in>I. g i) \<le> (SUP i\<in>I. f i + g i)" .
   qed
 qed
 
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -2149,23 +2149,23 @@
   unfolding continuous_def by auto
 
 lemma ereal_Sup:
-  assumes *: "\<bar>SUP a:A. ereal a\<bar> \<noteq> \<infinity>"
-  shows "ereal (Sup A) = (SUP a:A. ereal a)"
+  assumes *: "\<bar>SUP a\<in>A. ereal a\<bar> \<noteq> \<infinity>"
+  shows "ereal (Sup A) = (SUP a\<in>A. ereal a)"
 proof (rule continuous_at_Sup_mono)
-  obtain r where r: "ereal r = (SUP a:A. ereal a)" "A \<noteq> {}"
+  obtain r where r: "ereal r = (SUP a\<in>A. ereal a)" "A \<noteq> {}"
     using * by (force simp: bot_ereal_def)
   then show "bdd_above A" "A \<noteq> {}"
     by (auto intro!: SUP_upper bdd_aboveI[of _ r] simp flip: ereal_less_eq)
 qed (auto simp: mono_def continuous_at_imp_continuous_at_within continuous_at_ereal)
 
-lemma ereal_SUP: "\<bar>SUP a:A. ereal (f a)\<bar> \<noteq> \<infinity> \<Longrightarrow> ereal (SUP a:A. f a) = (SUP a:A. ereal (f a))"
+lemma ereal_SUP: "\<bar>SUP a\<in>A. ereal (f a)\<bar> \<noteq> \<infinity> \<Longrightarrow> ereal (SUP a\<in>A. f a) = (SUP a\<in>A. ereal (f a))"
   using ereal_Sup[of "f`A"] by auto
 
 lemma ereal_Inf:
-  assumes *: "\<bar>INF a:A. ereal a\<bar> \<noteq> \<infinity>"
-  shows "ereal (Inf A) = (INF a:A. ereal a)"
+  assumes *: "\<bar>INF a\<in>A. ereal a\<bar> \<noteq> \<infinity>"
+  shows "ereal (Inf A) = (INF a\<in>A. ereal a)"
 proof (rule continuous_at_Inf_mono)
-  obtain r where r: "ereal r = (INF a:A. ereal a)" "A \<noteq> {}"
+  obtain r where r: "ereal r = (INF a\<in>A. ereal a)" "A \<noteq> {}"
     using * by (force simp: top_ereal_def)
   then show "bdd_below A" "A \<noteq> {}"
     by (auto intro!: INF_lower bdd_belowI[of _ r] simp flip: ereal_less_eq)
@@ -2173,17 +2173,17 @@
 
 lemma ereal_Inf':
   assumes *: "bdd_below A" "A \<noteq> {}"
-  shows "ereal (Inf A) = (INF a:A. ereal a)"
+  shows "ereal (Inf A) = (INF a\<in>A. ereal a)"
 proof (rule ereal_Inf)
   from * obtain l u where "x \<in> A \<Longrightarrow> l \<le> x" "u \<in> A" for x
     by (auto simp: bdd_below_def)
-  then have "l \<le> (INF x:A. ereal x)" "(INF x:A. ereal x) \<le> u"
+  then have "l \<le> (INF x\<in>A. ereal x)" "(INF x\<in>A. ereal x) \<le> u"
     by (auto intro!: INF_greatest INF_lower)
-  then show "\<bar>INF a:A. ereal a\<bar> \<noteq> \<infinity>"
+  then show "\<bar>INF a\<in>A. ereal a\<bar> \<noteq> \<infinity>"
     by auto
 qed
 
-lemma ereal_INF: "\<bar>INF a:A. ereal (f a)\<bar> \<noteq> \<infinity> \<Longrightarrow> ereal (INF a:A. f a) = (INF a:A. ereal (f a))"
+lemma ereal_INF: "\<bar>INF a\<in>A. ereal (f a)\<bar> \<noteq> \<infinity> \<Longrightarrow> ereal (INF a\<in>A. f a) = (INF a\<in>A. ereal (f a))"
   using ereal_Inf[of "f`A"] by auto
 
 lemma ereal_Sup_uminus_image_eq: "Sup (uminus ` S::ereal set) = - Inf S"
@@ -2193,7 +2193,7 @@
 
 lemma ereal_SUP_uminus_eq:
   fixes f :: "'a \<Rightarrow> ereal"
-  shows "(SUP x:S. uminus (f x)) = - (INF x:S. f x)"
+  shows "(SUP x\<in>S. uminus (f x)) = - (INF x\<in>S. f x)"
   using ereal_Sup_uminus_image_eq [of "f ` S"] by (simp add: comp_def)
 
 lemma ereal_inj_on_uminus[intro, simp]: "inj_on uminus (A :: ereal set)"
@@ -2204,12 +2204,12 @@
 
 lemma ereal_INF_uminus_eq:
   fixes f :: "'a \<Rightarrow> ereal"
-  shows "(INF x:S. - f x) = - (SUP x:S. f x)"
+  shows "(INF x\<in>S. - f x) = - (SUP x\<in>S. f x)"
   using ereal_Inf_uminus_image_eq [of "f ` S"] by (simp add: comp_def)
 
 lemma ereal_SUP_uminus:
   fixes f :: "'a \<Rightarrow> ereal"
-  shows "(SUP i : R. - f i) = - (INF i : R. f i)"
+  shows "(SUP i \<in> R. - f i) = - (INF i \<in> R. f i)"
   using ereal_Sup_uminus_image_eq[of "f`R"]
   by (simp add: image_image)
 
@@ -2278,17 +2278,17 @@
 qed
 
 lemma SUP_PInfty:
-  "(\<And>n::nat. \<exists>i\<in>A. ereal (real n) \<le> f i) \<Longrightarrow> (SUP i:A. f i :: ereal) = \<infinity>"
+  "(\<And>n::nat. \<exists>i\<in>A. ereal (real n) \<le> f i) \<Longrightarrow> (SUP i\<in>A. f i :: ereal) = \<infinity>"
   unfolding top_ereal_def[symmetric] SUP_eq_top_iff
   by (metis MInfty_neq_PInfty(2) PInfty_neq_ereal(2) less_PInf_Ex_of_nat less_ereal.elims(2) less_le_trans)
 
-lemma SUP_nat_Infty: "(SUP i::nat. ereal (real i)) = \<infinity>"
+lemma SUP_nat_Infty: "(SUP i. ereal (real i)) = \<infinity>"
   by (rule SUP_PInfty) auto
 
 lemma SUP_ereal_add_left:
   assumes "I \<noteq> {}" "c \<noteq> -\<infinity>"
-  shows "(SUP i:I. f i + c :: ereal) = (SUP i:I. f i) + c"
-proof (cases "(SUP i:I. f i) = - \<infinity>")
+  shows "(SUP i\<in>I. f i + c :: ereal) = (SUP i\<in>I. f i) + c"
+proof (cases "(SUP i\<in>I. f i) = - \<infinity>")
   case True
   then have "\<And>i. i \<in> I \<Longrightarrow> f i = -\<infinity>"
     unfolding Sup_eq_MInfty by auto
@@ -2303,23 +2303,23 @@
 
 lemma SUP_ereal_add_right:
   fixes c :: ereal
-  shows "I \<noteq> {} \<Longrightarrow> c \<noteq> -\<infinity> \<Longrightarrow> (SUP i:I. c + f i) = c + (SUP i:I. f i)"
+  shows "I \<noteq> {} \<Longrightarrow> c \<noteq> -\<infinity> \<Longrightarrow> (SUP i\<in>I. c + f i) = c + (SUP i\<in>I. f i)"
   using SUP_ereal_add_left[of I c f] by (simp add: add.commute)
 
 lemma SUP_ereal_minus_right:
   assumes "I \<noteq> {}" "c \<noteq> -\<infinity>"
-  shows "(SUP i:I. c - f i :: ereal) = c - (INF i:I. f i)"
+  shows "(SUP i\<in>I. c - f i :: ereal) = c - (INF i\<in>I. f i)"
   using SUP_ereal_add_right[OF assms, of "\<lambda>i. - f i"]
   by (simp add: ereal_SUP_uminus minus_ereal_def)
 
 lemma SUP_ereal_minus_left:
   assumes "I \<noteq> {}" "c \<noteq> \<infinity>"
-  shows "(SUP i:I. f i - c:: ereal) = (SUP i:I. f i) - c"
+  shows "(SUP i\<in>I. f i - c:: ereal) = (SUP i\<in>I. f i) - c"
   using SUP_ereal_add_left[OF \<open>I \<noteq> {}\<close>, of "-c" f] by (simp add: \<open>c \<noteq> \<infinity>\<close> minus_ereal_def)
 
 lemma INF_ereal_minus_right:
   assumes "I \<noteq> {}" and "\<bar>c\<bar> \<noteq> \<infinity>"
-  shows "(INF i:I. c - f i) = c - (SUP i:I. f i::ereal)"
+  shows "(INF i\<in>I. c - f i) = c - (SUP i\<in>I. f i::ereal)"
 proof -
   { fix b have "(-c) + b = - (c - b)"
       using \<open>\<bar>c\<bar> \<noteq> \<infinity>\<close> by (cases c b rule: ereal2_cases) auto }
@@ -2339,7 +2339,7 @@
 lemma SUP_combine:
   fixes f :: "'a::semilattice_sup \<Rightarrow> 'a::semilattice_sup \<Rightarrow> 'b::complete_lattice"
   assumes mono: "\<And>a b c d. a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> f a c \<le> f b d"
-  shows "(SUP i:UNIV. SUP j:UNIV. f i j) = (SUP i. f i i)"
+  shows "(SUP i\<in>UNIV. SUP j\<in>UNIV. f i j) = (SUP i. f i i)"
 proof (rule antisym)
   show "(SUP i j. f i j) \<le> (SUP i. f i i)"
     by (rule SUP_least SUP_upper2[where i="sup i j" for i j] UNIV_I mono sup_ge1 sup_ge2)+
@@ -2360,14 +2360,14 @@
   apply (rule SUP_combine[symmetric] add_mono inc[THEN monoD] | assumption)+
   done
 
-lemma INF_eq_minf: "(INF i:I. f i::ereal) \<noteq> -\<infinity> \<longleftrightarrow> (\<exists>b>-\<infinity>. \<forall>i\<in>I. b \<le> f i)"
+lemma INF_eq_minf: "(INF i\<in>I. f i::ereal) \<noteq> -\<infinity> \<longleftrightarrow> (\<exists>b>-\<infinity>. \<forall>i\<in>I. b \<le> f i)"
   unfolding bot_ereal_def[symmetric] INF_eq_bot_iff by (auto simp: not_less)
 
 lemma INF_ereal_add_left:
   assumes "I \<noteq> {}" "c \<noteq> -\<infinity>" "\<And>x. x \<in> I \<Longrightarrow> 0 \<le> f x"
-  shows "(INF i:I. f i + c :: ereal) = (INF i:I. f i) + c"
+  shows "(INF i\<in>I. f i + c :: ereal) = (INF i\<in>I. f i) + c"
 proof -
-  have "(INF i:I. f i) \<noteq> -\<infinity>"
+  have "(INF i\<in>I. f i) \<noteq> -\<infinity>"
     unfolding INF_eq_minf using assms by (intro exI[of _ 0]) auto
   then show ?thesis
     by (subst continuous_at_Inf_mono[where f="\<lambda>x. x + c"])
@@ -2376,14 +2376,14 @@
 
 lemma INF_ereal_add_right:
   assumes "I \<noteq> {}" "c \<noteq> -\<infinity>" "\<And>x. x \<in> I \<Longrightarrow> 0 \<le> f x"
-  shows "(INF i:I. c + f i :: ereal) = c + (INF i:I. f i)"
+  shows "(INF i\<in>I. c + f i :: ereal) = c + (INF i\<in>I. f i)"
   using INF_ereal_add_left[OF assms] by (simp add: ac_simps)
 
 lemma INF_ereal_add_directed:
   fixes f g :: "'a \<Rightarrow> ereal"
   assumes nonneg: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> g i"
   assumes directed: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> \<exists>k\<in>I. f i + g j \<ge> f k + g k"
-  shows "(INF i:I. f i + g i) = (INF i:I. f i) + (INF i:I. g i)"
+  shows "(INF i\<in>I. f i + g i) = (INF i\<in>I. f i) + (INF i\<in>I. g i)"
 proof cases
   assume "I = {}" then show ?thesis
     by (simp add: top_ereal_def)
@@ -2391,16 +2391,16 @@
   assume "I \<noteq> {}"
   show ?thesis
   proof (rule antisym)
-    show "(INF i:I. f i) + (INF i:I. g i) \<le> (INF i:I. f i + g i)"
+    show "(INF i\<in>I. f i) + (INF i\<in>I. g i) \<le> (INF i\<in>I. f i + g i)"
       by (rule INF_greatest; intro add_mono INF_lower)
   next
-    have "(INF i:I. f i + g i) \<le> (INF i:I. (INF j:I. f i + g j))"
+    have "(INF i\<in>I. f i + g i) \<le> (INF i\<in>I. (INF j\<in>I. f i + g j))"
       using directed by (intro INF_greatest) (blast intro: INF_lower2)
-    also have "\<dots> = (INF i:I. f i + (INF i:I. g i))"
+    also have "\<dots> = (INF i\<in>I. f i + (INF i\<in>I. g i))"
       using nonneg by (intro INF_cong refl INF_ereal_add_right \<open>I \<noteq> {}\<close>) (auto simp: INF_eq_minf intro!: exI[of _ 0])
-    also have "\<dots> = (INF i:I. f i) + (INF i:I. g i)"
+    also have "\<dots> = (INF i\<in>I. f i) + (INF i\<in>I. g i)"
       using nonneg by (intro INF_ereal_add_left \<open>I \<noteq> {}\<close>) (auto simp: INF_eq_minf intro!: exI[of _ 0])
-    finally show "(INF i:I. f i + g i) \<le> (INF i:I. f i) + (INF i:I. g i)" .
+    finally show "(INF i\<in>I. f i + g i) \<le> (INF i\<in>I. f i) + (INF i\<in>I. g i)" .
   qed
 qed
 
@@ -2454,8 +2454,8 @@
   fixes f :: "'a \<Rightarrow> ereal"
   assumes "I \<noteq> {}"
   assumes f: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" and c: "0 \<le> c"
-  shows "(SUP i:I. c * f i) = c * (SUP i:I. f i)"
-proof (cases "(SUP i: I. f i) = 0")
+  shows "(SUP i\<in>I. c * f i) = c * (SUP i\<in>I. f i)"
+proof (cases "(SUP i \<in> I. f i) = 0")
   case True
   then have "\<And>i. i \<in> I \<Longrightarrow> f i = 0"
     by (metis SUP_upper f antisym)
@@ -2595,9 +2595,9 @@
 by(cases n) simp_all
 
 lemma ereal_of_enat_Sup:
-  assumes "A \<noteq> {}" shows "ereal_of_enat (Sup A) = (SUP a : A. ereal_of_enat a)"
+  assumes "A \<noteq> {}" shows "ereal_of_enat (Sup A) = (SUP a \<in> A. ereal_of_enat a)"
 proof (intro antisym mono_Sup)
-  show "ereal_of_enat (Sup A) \<le> (SUP a : A. ereal_of_enat a)"
+  show "ereal_of_enat (Sup A) \<le> (SUP a \<in> A. ereal_of_enat a)"
   proof cases
     assume "finite A"
     with \<open>A \<noteq> {}\<close> obtain a where "a \<in> A" "ereal_of_enat (Sup A) = ereal_of_enat a"
@@ -2606,7 +2606,7 @@
       by (auto intro: SUP_upper)
   next
     assume "\<not> finite A"
-    have [simp]: "(SUP a : A. ereal_of_enat a) = top"
+    have [simp]: "(SUP a \<in> A. ereal_of_enat a) = top"
       unfolding SUP_eq_top_iff
     proof safe
       fix x :: ereal assume "x < top"
@@ -2626,7 +2626,7 @@
 qed (simp add: mono_def)
 
 lemma ereal_of_enat_SUP:
-  "A \<noteq> {} \<Longrightarrow> ereal_of_enat (SUP a:A. f a) = (SUP a : A. ereal_of_enat (f a))"
+  "A \<noteq> {} \<Longrightarrow> ereal_of_enat (SUP a\<in>A. f a) = (SUP a \<in> A. ereal_of_enat (f a))"
   using ereal_of_enat_Sup[of "f`A"] by auto
 
 subsection "Limits on @{typ ereal}"
@@ -3225,43 +3225,43 @@
   let ?INF = "\<lambda>P g. INFIMUM (Collect P) g"
   show "?F \<noteq> {}"
     by (auto intro: eventually_True)
-  show "(SUP P:?F. ?INF P g) \<noteq> - \<infinity>"
+  show "(SUP P\<in>?F. ?INF P g) \<noteq> - \<infinity>"
     unfolding bot_ereal_def[symmetric] SUP_bot_conv INF_eq_bot_iff
     by (auto intro!: exI[of _ 0] ev simp: bot_ereal_def)
-  have "(SUP P:?F. ?INF P f + (SUP P:?F. ?INF P g)) \<le> (SUP P:?F. (SUP P':?F. ?INF P f + ?INF P' g))"
+  have "(SUP P\<in>?F. ?INF P f + (SUP P\<in>?F. ?INF P g)) \<le> (SUP P\<in>?F. (SUP P'\<in>?F. ?INF P f + ?INF P' g))"
   proof (safe intro!: SUP_mono bexI[of _ "\<lambda>x. P x \<and> 0 \<le> f x" for P])
     fix P let ?P' = "\<lambda>x. P x \<and> 0 \<le> f x"
     assume "eventually P F"
     with ev show "eventually ?P' F"
       by eventually_elim auto
-    have "?INF P f + (SUP P:?F. ?INF P g) \<le> ?INF ?P' f + (SUP P:?F. ?INF P g)"
+    have "?INF P f + (SUP P\<in>?F. ?INF P g) \<le> ?INF ?P' f + (SUP P\<in>?F. ?INF P g)"
       by (intro add_mono INF_mono) auto
-    also have "\<dots> = (SUP P':?F. ?INF ?P' f + ?INF P' g)"
+    also have "\<dots> = (SUP P'\<in>?F. ?INF ?P' f + ?INF P' g)"
     proof (rule SUP_ereal_add_right[symmetric])
       show "INFIMUM {x. P x \<and> 0 \<le> f x} f \<noteq> - \<infinity>"
         unfolding bot_ereal_def[symmetric] INF_eq_bot_iff
         by (auto intro!: exI[of _ 0] ev simp: bot_ereal_def)
     qed fact
-    finally show "?INF P f + (SUP P:?F. ?INF P g) \<le> (SUP P':?F. ?INF ?P' f + ?INF P' g)" .
+    finally show "?INF P f + (SUP P\<in>?F. ?INF P g) \<le> (SUP P'\<in>?F. ?INF ?P' f + ?INF P' g)" .
   qed
-  also have "\<dots> \<le> (SUP P:?F. INF x:Collect P. f x + g x)"
+  also have "\<dots> \<le> (SUP P\<in>?F. INF x\<in>Collect P. f x + g x)"
   proof (safe intro!: SUP_least)
     fix P Q assume *: "eventually P F" "eventually Q F"
-    show "?INF P f + ?INF Q g \<le> (SUP P:?F. INF x:Collect P. f x + g x)"
+    show "?INF P f + ?INF Q g \<le> (SUP P\<in>?F. INF x\<in>Collect P. f x + g x)"
     proof (rule SUP_upper2)
       show "(\<lambda>x. P x \<and> Q x) \<in> ?F"
         using * by (auto simp: eventually_conj)
-      show "?INF P f + ?INF Q g \<le> (INF x:{x. P x \<and> Q x}. f x + g x)"
+      show "?INF P f + ?INF Q g \<le> (INF x\<in>{x. P x \<and> Q x}. f x + g x)"
         by (intro INF_greatest add_mono) (auto intro: INF_lower)
     qed
   qed
-  finally show "(SUP P:?F. ?INF P f + (SUP P:?F. ?INF P g)) \<le> (SUP P:?F. INF x:Collect P. f x + g x)" .
+  finally show "(SUP P\<in>?F. ?INF P f + (SUP P\<in>?F. ?INF P g)) \<le> (SUP P\<in>?F. INF x\<in>Collect P. f x + g x)" .
 qed
 
 lemma Sup_ereal_mult_right':
   assumes nonempty: "Y \<noteq> {}"
   and x: "x \<ge> 0"
-  shows "(SUP i:Y. f i) * ereal x = (SUP i:Y. f i * ereal x)" (is "?lhs = ?rhs")
+  shows "(SUP i\<in>Y. f i) * ereal x = (SUP i\<in>Y. f i * ereal x)" (is "?lhs = ?rhs")
 proof(cases "x = 0")
   case True thus ?thesis by(auto simp add: nonempty zero_ereal_def[symmetric])
 next
@@ -3271,8 +3271,8 @@
     show "?rhs \<le> ?lhs"
       by(rule SUP_least)(simp add: ereal_mult_right_mono SUP_upper x)
   next
-    have "?lhs / ereal x = (SUP i:Y. f i) * (ereal x / ereal x)" by(simp only: ereal_times_divide_eq)
-    also have "\<dots> = (SUP i:Y. f i)" using False by simp
+    have "?lhs / ereal x = (SUP i\<in>Y. f i) * (ereal x / ereal x)" by(simp only: ereal_times_divide_eq)
+    also have "\<dots> = (SUP i\<in>Y. f i)" using False by simp
     also have "\<dots> \<le> ?rhs / x"
     proof(rule SUP_least)
       fix i
@@ -3292,7 +3292,7 @@
 qed
 
 lemma Sup_ereal_mult_left':
-  "\<lbrakk> Y \<noteq> {}; x \<ge> 0 \<rbrakk> \<Longrightarrow> ereal x * (SUP i:Y. f i) = (SUP i:Y. ereal x * f i)"
+  "\<lbrakk> Y \<noteq> {}; x \<ge> 0 \<rbrakk> \<Longrightarrow> ereal x * (SUP i\<in>Y. f i) = (SUP i\<in>Y. ereal x * f i)"
 by(subst (1 2) mult.commute)(rule Sup_ereal_mult_right')
 
 lemma sup_continuous_add[order_continuous_intros]:
@@ -3676,7 +3676,7 @@
   fixes f g :: "'a \<Rightarrow> ereal"
   assumes nonneg: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> g i"
   assumes directed: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> \<exists>k\<in>I. f i + g j \<le> f k + g k"
-  shows "(SUP i:I. f i + g i) = (SUP i:I. f i) + (SUP i:I. g i)"
+  shows "(SUP i\<in>I. f i + g i) = (SUP i\<in>I. f i) + (SUP i\<in>I. g i)"
 proof cases
   assume "I = {}" then show ?thesis
     by (simp add: bot_ereal_def)
@@ -3684,18 +3684,18 @@
   assume "I \<noteq> {}"
   show ?thesis
   proof (rule antisym)
-    show "(SUP i:I. f i + g i) \<le> (SUP i:I. f i) + (SUP i:I. g i)"
+    show "(SUP i\<in>I. f i + g i) \<le> (SUP i\<in>I. f i) + (SUP i\<in>I. g i)"
       by (rule SUP_least; intro add_mono SUP_upper)
   next
-    have "bot < (SUP i:I. g i)"
+    have "bot < (SUP i\<in>I. g i)"
       using \<open>I \<noteq> {}\<close> nonneg(2) by (auto simp: bot_ereal_def less_SUP_iff)
-    then have "(SUP i:I. f i) + (SUP i:I. g i) = (SUP i:I. f i + (SUP i:I. g i))"
+    then have "(SUP i\<in>I. f i) + (SUP i\<in>I. g i) = (SUP i\<in>I. f i + (SUP i\<in>I. g i))"
       by (intro SUP_ereal_add_left[symmetric] \<open>I \<noteq> {}\<close>) auto
-    also have "\<dots> = (SUP i:I. (SUP j:I. f i + g j))"
+    also have "\<dots> = (SUP i\<in>I. (SUP j\<in>I. f i + g j))"
       using nonneg(1) by (intro SUP_cong refl SUP_ereal_add_right[symmetric] \<open>I \<noteq> {}\<close>) auto
-    also have "\<dots> \<le> (SUP i:I. f i + g i)"
+    also have "\<dots> \<le> (SUP i\<in>I. f i + g i)"
       using directed by (intro SUP_least) (blast intro: SUP_upper2)
-    finally show "(SUP i:I. f i) + (SUP i:I. g i) \<le> (SUP i:I. f i + g i)" .
+    finally show "(SUP i\<in>I. f i) + (SUP i\<in>I. g i) \<le> (SUP i\<in>I. f i + g i)" .
   qed
 qed
 
@@ -3704,12 +3704,12 @@
   assumes "I \<noteq> {}"
   assumes directed: "\<And>N i j. N \<subseteq> A \<Longrightarrow> i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> \<exists>k\<in>I. \<forall>n\<in>N. f n i \<le> f n k \<and> f n j \<le> f n k"
   assumes nonneg: "\<And>n i. i \<in> I \<Longrightarrow> n \<in> A \<Longrightarrow> 0 \<le> f n i"
-  shows "(SUP i:I. \<Sum>n\<in>A. f n i) = (\<Sum>n\<in>A. SUP i:I. f n i)"
+  shows "(SUP i\<in>I. \<Sum>n\<in>A. f n i) = (\<Sum>n\<in>A. SUP i\<in>I. f n i)"
 proof -
-  have "N \<subseteq> A \<Longrightarrow> (SUP i:I. \<Sum>n\<in>N. f n i) = (\<Sum>n\<in>N. SUP i:I. f n i)" for N
+  have "N \<subseteq> A \<Longrightarrow> (SUP i\<in>I. \<Sum>n\<in>N. f n i) = (\<Sum>n\<in>N. SUP i\<in>I. f n i)" for N
   proof (induction N rule: infinite_finite_induct)
     case (insert n N)
-    moreover have "(SUP i:I. f n i + (\<Sum>l\<in>N. f l i)) = (SUP i:I. f n i) + (SUP i:I. \<Sum>l\<in>N. f l i)"
+    moreover have "(SUP i\<in>I. f n i + (\<Sum>l\<in>N. f l i)) = (SUP i\<in>I. f n i) + (SUP i\<in>I. \<Sum>l\<in>N. f l i)"
     proof (rule SUP_ereal_add_directed)
       fix i assume "i \<in> I" then show "0 \<le> f n i" "0 \<le> (\<Sum>l\<in>N. f l i)"
         using insert by (auto intro!: sum_nonneg nonneg)
@@ -3730,11 +3730,11 @@
   assumes "I \<noteq> {}"
   assumes directed: "\<And>N i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> finite N \<Longrightarrow> \<exists>k\<in>I. \<forall>n\<in>N. f i n \<le> f k n \<and> f j n \<le> f k n"
   assumes nonneg: "\<And>n i. 0 \<le> f n i"
-  shows "(\<Sum>i. SUP n:I. f n i) = (SUP n:I. \<Sum>i. f n i)"
+  shows "(\<Sum>i. SUP n\<in>I. f n i) = (SUP n\<in>I. \<Sum>i. f n i)"
 proof (subst (1 2) suminf_ereal_eq_SUP)
-  show "\<And>n i. 0 \<le> f n i" "\<And>i. 0 \<le> (SUP n:I. f n i)"
+  show "\<And>n i. 0 \<le> f n i" "\<And>i. 0 \<le> (SUP n\<in>I. f n i)"
     using \<open>I \<noteq> {}\<close> nonneg by (auto intro: SUP_upper2)
-  show "(SUP n. \<Sum>i<n. SUP n:I. f n i) = (SUP n:I. SUP j. \<Sum>i<j. f n i)"
+  show "(SUP n. \<Sum>i<n. SUP n\<in>I. f n i) = (SUP n\<in>I. SUP j. \<Sum>i<j. f n i)"
     apply (subst SUP_commute)
     apply (subst SUP_ereal_sum_directed)
     apply (auto intro!: assms simp: finite_subset)
@@ -4223,11 +4223,11 @@
   fixes f :: "_ \<Rightarrow> ereal" and A
   assumes nonneg: "\<forall>x\<in>A. f x \<ge> 0"
   and A:"A \<noteq> {}"
-  shows "(SUP x:A. f x) = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)" (is "?lhs \<longleftrightarrow> ?rhs")
+  shows "(SUP x\<in>A. f x) = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)" (is "?lhs \<longleftrightarrow> ?rhs")
 proof(intro iffI ballI)
   fix x
   assume "?lhs" "x \<in> A"
-  from \<open>x \<in> A\<close> have "f x \<le> (SUP x:A. f x)" by(rule SUP_upper)
+  from \<open>x \<in> A\<close> have "f x \<le> (SUP x\<in>A. f x)" by(rule SUP_upper)
   with \<open>?lhs\<close> show "f x = 0" using nonneg \<open>x \<in> A\<close> by auto
 qed(simp cong: SUP_cong add: A)
 
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Library/Finite_Lattice.thy
--- a/src/HOL/Library/Finite_Lattice.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Library/Finite_Lattice.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -159,12 +159,12 @@
   distrib_lattice + finite_lattice_complete
 
 lemma finite_distrib_lattice_complete_sup_Inf:
-  "sup (x::'a::finite_distrib_lattice_complete) (Inf A) = (INF y:A. sup x y)"
+  "sup (x::'a::finite_distrib_lattice_complete) (Inf A) = (INF y\<in>A. sup x y)"
   using finite
   by (induct A rule: finite_induct) (simp_all add: sup_inf_distrib1)
 
 lemma finite_distrib_lattice_complete_inf_Sup:
-  "inf (x::'a::finite_distrib_lattice_complete) (Sup A) = (SUP y:A. inf x y)"
+  "inf (x::'a::finite_distrib_lattice_complete) (Sup A) = (SUP y\<in>A. inf x y)"
   using finite [of A] by induct (simp_all add: inf_sup_distrib1)
 
 context finite_distrib_lattice_complete
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Library/Liminf_Limsup.thy
--- a/src/HOL/Library/Liminf_Limsup.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Library/Liminf_Limsup.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -25,13 +25,13 @@
 
 lemma le_cSup_iff_less:
   fixes x :: "'a :: {conditionally_complete_linorder, dense_linorder}"
-  shows "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> x \<le> (SUP i:A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)"
+  shows "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> x \<le> (SUP i\<in>A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)"
   by (simp add: le_cSUP_iff)
      (blast intro: less_imp_le less_trans less_le_trans dest: dense)
 
 lemma le_Sup_iff_less:
   fixes x :: "'a :: {complete_linorder, dense_linorder}"
-  shows "x \<le> (SUP i:A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)" (is "?lhs = ?rhs")
+  shows "x \<le> (SUP i\<in>A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)" (is "?lhs = ?rhs")
   unfolding le_SUP_iff
   by (blast intro: less_imp_le less_trans less_le_trans dest: dense)
 
@@ -51,38 +51,38 @@
 
 lemma cInf_le_iff_less:
   fixes x :: "'a :: {conditionally_complete_linorder, dense_linorder}"
-  shows "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> (INF i:A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)"
+  shows "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> (INF i\<in>A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)"
   by (simp add: cINF_le_iff)
      (blast intro: less_imp_le less_trans le_less_trans dest: dense)
 
 lemma Inf_le_iff_less:
   fixes x :: "'a :: {complete_linorder, dense_linorder}"
-  shows "(INF i:A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)"
+  shows "(INF i\<in>A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)"
   unfolding INF_le_iff
   by (blast intro: less_imp_le less_trans le_less_trans dest: dense)
 
 lemma SUP_pair:
   fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice"
-  shows "(SUP i : A. SUP j : B. f i j) = (SUP p : A \<times> B. f (fst p) (snd p))"
+  shows "(SUP i \<in> A. SUP j \<in> B. f i j) = (SUP p \<in> A \<times> B. f (fst p) (snd p))"
   by (rule antisym) (auto intro!: SUP_least SUP_upper2)
 
 lemma INF_pair:
   fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice"
-  shows "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))"
+  shows "(INF i \<in> A. INF j \<in> B. f i j) = (INF p \<in> A \<times> B. f (fst p) (snd p))"
   by (rule antisym) (auto intro!: INF_greatest INF_lower2)
 
 lemma INF_Sigma:
   fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice"
-  shows "(INF i : A. INF j : B i. f i j) = (INF p : Sigma A B. f (fst p) (snd p))"
+  shows "(INF i \<in> A. INF j \<in> B i. f i j) = (INF p \<in> Sigma A B. f (fst p) (snd p))"
   by (rule antisym) (auto intro!: INF_greatest INF_lower2)
 
 subsubsection \<open>\<open>Liminf\<close> and \<open>Limsup\<close>\<close>
 
 definition Liminf :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b :: complete_lattice" where
-  "Liminf F f = (SUP P:{P. eventually P F}. INF x:{x. P x}. f x)"
+  "Liminf F f = (SUP P\<in>{P. eventually P F}. INF x\<in>{x. P x}. f x)"
 
 definition Limsup :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b :: complete_lattice" where
-  "Limsup F f = (INF P:{P. eventually P F}. SUP x:{x. P x}. f x)"
+  "Limsup F f = (INF P\<in>{P. eventually P F}. SUP x\<in>{x. P x}. f x)"
 
 abbreviation "liminf \<equiv> Liminf sequentially"
 
@@ -98,11 +98,11 @@
     (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPREMUM (Collect P) f) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x"
   unfolding Limsup_def by (auto intro!: INF_eqI)
 
-lemma liminf_SUP_INF: "liminf f = (SUP n. INF m:{n..}. f m)"
+lemma liminf_SUP_INF: "liminf f = (SUP n. INF m\<in>{n..}. f m)"
   unfolding Liminf_def eventually_sequentially
   by (rule SUP_eq) (auto simp: atLeast_def intro!: INF_mono)
 
-lemma limsup_INF_SUP: "limsup f = (INF n. SUP m:{n..}. f m)"
+lemma limsup_INF_SUP: "limsup f = (INF n. SUP m\<in>{n..}. f m)"
   unfolding Limsup_def eventually_sequentially
   by (rule INF_eq) (auto simp: atLeast_def intro!: SUP_mono)
 
@@ -111,7 +111,7 @@
   shows "Limsup F (\<lambda>x. c) = c"
 proof -
   have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
-  have "\<And>P. eventually P F \<Longrightarrow> (SUP x : {x. P x}. c) = c"
+  have "\<And>P. eventually P F \<Longrightarrow> (SUP x \<in> {x. P x}. c) = c"
     using ntriv by (intro SUP_const) (auto simp: eventually_False *)
   then show ?thesis
     unfolding Limsup_def using eventually_True
@@ -124,7 +124,7 @@
   shows "Liminf F (\<lambda>x. c) = c"
 proof -
   have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
-  have "\<And>P. eventually P F \<Longrightarrow> (INF x : {x. P x}. c) = c"
+  have "\<And>P. eventually P F \<Longrightarrow> (INF x \<in> {x. P x}. c) = c"
     using ntriv by (intro INF_const) (auto simp: eventually_False *)
   then show ?thesis
     unfolding Liminf_def using eventually_True
@@ -387,7 +387,7 @@
   assumes "strict_mono r"
   shows "liminf X \<le> liminf (X \<circ> r) "
 proof-
-  have "\<And>n. (INF m:{n..}. X m) \<le> (INF m:{n..}. (X \<circ> r) m)"
+  have "\<And>n. (INF m\<in>{n..}. X m) \<le> (INF m\<in>{n..}. (X \<circ> r) m)"
   proof (safe intro!: INF_mono)
     fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m"
       using seq_suble[OF \<open>strict_mono r\<close>, of m] by (intro bexI[of _ "r m"]) auto
@@ -400,7 +400,7 @@
   assumes "strict_mono r"
   shows "limsup (X \<circ> r) \<le> limsup X"
 proof-
-  have "(SUP m:{n..}. (X \<circ> r) m) \<le> (SUP m:{n..}. X m)" for n
+  have "(SUP m\<in>{n..}. (X \<circ> r) m) \<le> (SUP m\<in>{n..}. X m)" for n
   proof (safe intro!: SUP_mono)
     fix m :: nat
     assume "n \<le> m"
@@ -431,11 +431,11 @@
     qed }
   note * = this
 
-  have "f (Liminf F g) = (SUP P : {P. eventually P F}. f (Inf (g ` Collect P)))"
+  have "f (Liminf F g) = (SUP P \<in> {P. eventually P F}. f (Inf (g ` Collect P)))"
     unfolding Liminf_def
     by (subst continuous_at_Sup_mono[OF am continuous_on_imp_continuous_within[OF c]])
        (auto intro: eventually_True)
-  also have "\<dots> = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)"
+  also have "\<dots> = (SUP P \<in> {P. eventually P F}. INFIMUM (g ` Collect P) f)"
     by (intro SUP_cong refl continuous_at_Inf_mono[OF am continuous_on_imp_continuous_within[OF c]])
        (auto dest!: eventually_happens simp: F)
   finally show ?thesis by (auto simp: Liminf_def)
@@ -456,11 +456,11 @@
     qed }
   note * = this
 
-  have "f (Limsup F g) = (INF P : {P. eventually P F}. f (Sup (g ` Collect P)))"
+  have "f (Limsup F g) = (INF P \<in> {P. eventually P F}. f (Sup (g ` Collect P)))"
     unfolding Limsup_def
     by (subst continuous_at_Inf_mono[OF am continuous_on_imp_continuous_within[OF c]])
        (auto intro: eventually_True)
-  also have "\<dots> = (INF P : {P. eventually P F}. SUPREMUM (g ` Collect P) f)"
+  also have "\<dots> = (INF P \<in> {P. eventually P F}. SUPREMUM (g ` Collect P) f)"
     by (intro INF_cong refl continuous_at_Sup_mono[OF am continuous_on_imp_continuous_within[OF c]])
        (auto dest!: eventually_happens simp: F)
   finally show ?thesis by (auto simp: Limsup_def)
@@ -480,11 +480,11 @@
     with \<open>eventually P F\<close> F show False
       by auto
   qed
-  have "f (Limsup F g) = (SUP P : {P. eventually P F}. f (Sup (g ` Collect P)))"
+  have "f (Limsup F g) = (SUP P \<in> {P. eventually P F}. f (Sup (g ` Collect P)))"
     unfolding Limsup_def
     by (subst continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]])
        (auto intro: eventually_True)
-  also have "\<dots> = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)"
+  also have "\<dots> = (SUP P \<in> {P. eventually P F}. INFIMUM (g ` Collect P) f)"
     by (intro SUP_cong refl continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]])
        (auto dest!: eventually_happens simp: F)
   finally show ?thesis
@@ -506,11 +506,11 @@
     qed }
   note * = this
 
-  have "f (Liminf F g) = (INF P : {P. eventually P F}. f (Inf (g ` Collect P)))"
+  have "f (Liminf F g) = (INF P \<in> {P. eventually P F}. f (Inf (g ` Collect P)))"
     unfolding Liminf_def
     by (subst continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]])
        (auto intro: eventually_True)
-  also have "\<dots> = (INF P : {P. eventually P F}. SUPREMUM (g ` Collect P) f)"
+  also have "\<dots> = (INF P \<in> {P. eventually P F}. SUPREMUM (g ` Collect P) f)"
     by (intro INF_cong refl continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]])
        (auto dest!: eventually_happens simp: F)
   finally show ?thesis
@@ -527,10 +527,10 @@
   by (subst Limsup_def)
     (auto simp add: SUP_upper Limsup_bounded eventually_filtermap eventually_mono intro!: INF_greatest)
 
-lemma Liminf_least: "(\<And>P. eventually P F \<Longrightarrow> (INF x:Collect P. f x) \<le> x) \<Longrightarrow> Liminf F f \<le> x"
+lemma Liminf_least: "(\<And>P. eventually P F \<Longrightarrow> (INF x\<in>Collect P. f x) \<le> x) \<Longrightarrow> Liminf F f \<le> x"
   by (auto intro!: SUP_least simp: Liminf_def)
 
-lemma Limsup_greatest: "(\<And>P. eventually P F \<Longrightarrow> x \<le> (SUP x:Collect P. f x)) \<Longrightarrow> Limsup F f \<ge> x"
+lemma Limsup_greatest: "(\<And>P. eventually P F \<Longrightarrow> x \<le> (SUP x\<in>Collect P. f x)) \<Longrightarrow> Limsup F f \<ge> x"
   by (auto intro!: INF_greatest simp: Limsup_def)
 
 lemma Liminf_filtermap_ge: "inj f \<Longrightarrow> Liminf (filtermap f F) g \<ge> Liminf F (\<lambda>x. g (f x))"
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Library/Multiset.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -1035,7 +1035,7 @@
     ultimately have "finite {i. Inf ((\<lambda>f. f i) ` A) > 0}" by (rule finite_subset)
     with False show ?thesis by simp
   qed simp_all
-  thus "(\<lambda>i. if A = {} then 0 else INF f:A. f i) \<in> multiset" by (simp add: multiset_def)
+  thus "(\<lambda>i. if A = {} then 0 else INF f\<in>A. f i) \<in> multiset" by (simp add: multiset_def)
 qed
 
 instance ..
@@ -1094,17 +1094,17 @@
 
 lemma Sup_multiset_in_multiset:
   assumes "A \<noteq> {}" "subset_mset.bdd_above A"
-  shows   "(\<lambda>i. SUP X:A. count X i) \<in> multiset"
+  shows   "(\<lambda>i. SUP X\<in>A. count X i) \<in> multiset"
   unfolding multiset_def
 proof
   have "{i. Sup ((\<lambda>X. count X i) ` A) > 0} \<subseteq> (\<Union>X\<in>A. {i. 0 < count X i})"
   proof safe
-    fix i assume pos: "(SUP X:A. count X i) > 0"
+    fix i assume pos: "(SUP X\<in>A. count X i) > 0"
     show "i \<in> (\<Union>X\<in>A. {i. 0 < count X i})"
     proof (rule ccontr)
       assume "i \<notin> (\<Union>X\<in>A. {i. 0 < count X i})"
       hence "\<forall>X\<in>A. count X i \<le> 0" by (auto simp: count_eq_zero_iff)
-      with assms have "(SUP X:A. count X i) \<le> 0"
+      with assms have "(SUP X\<in>A. count X i) \<le> 0"
         by (intro cSup_least bdd_above_multiset_imp_bdd_above_count) auto
       with pos show False by simp
     qed
@@ -1115,7 +1115,7 @@
 
 lemma count_Sup_multiset_nonempty:
   assumes "A \<noteq> {}" "subset_mset.bdd_above A"
-  shows   "count (Sup A) x = (SUP X:A. count X x)"
+  shows   "count (Sup A) x = (SUP X\<in>A. count X x)"
   using assms by (simp add: Sup_multiset_def Abs_multiset_inverse Sup_multiset_in_multiset)
 
 
@@ -1127,7 +1127,7 @@
   proof (rule mset_subset_eqI)
     fix x
     from \<open>X \<in> A\<close> have "A \<noteq> {}" by auto
-    hence "count (Inf A) x = (INF X:A. count X x)"
+    hence "count (Inf A) x = (INF X\<in>A. count X x)"
       by (simp add: count_Inf_multiset_nonempty)
     also from \<open>X \<in> A\<close> have "\<dots> \<le> count X x"
       by (intro cInf_lower) simp_all
@@ -1139,7 +1139,7 @@
   show "X \<subseteq># Inf A"
   proof (rule mset_subset_eqI)
     fix x
-    from nonempty have "count X x \<le> (INF X:A. count X x)"
+    from nonempty have "count X x \<le> (INF X\<in>A. count X x)"
       by (intro cInf_greatest) (auto intro: mset_subset_eq_count le)
     also from nonempty have "\<dots> = count (Inf A) x" by (simp add: count_Inf_multiset_nonempty)
     finally show "count X x \<le> count (Inf A) x" .
@@ -1151,10 +1151,10 @@
   proof (rule mset_subset_eqI)
     fix x
     from X have "A \<noteq> {}" by auto
-    have "count X x \<le> (SUP X:A. count X x)"
+    have "count X x \<le> (SUP X\<in>A. count X x)"
       by (intro cSUP_upper X bdd_above_multiset_imp_bdd_above_count bdd)
     also from count_Sup_multiset_nonempty[OF \<open>A \<noteq> {}\<close> bdd]
-      have "(SUP X:A. count X x) = count (Sup A) x" by simp
+      have "(SUP X\<in>A. count X x) = count (Sup A) x" by simp
     finally show "count X x \<le> count (Sup A) x" .
   qed
 next
@@ -1165,7 +1165,7 @@
   proof (rule mset_subset_eqI)
     fix x
     from count_Sup_multiset_nonempty[OF \<open>A \<noteq> {}\<close> bdd]
-      have "count (Sup A) x = (SUP X:A. count X x)" .
+      have "count (Sup A) x = (SUP X\<in>A. count X x)" .
     also from nonempty have "\<dots> \<le> count X x"
       by (intro cSup_least) (auto intro: mset_subset_eq_count ge)
     finally show "count (Sup A) x \<le> count X x" .
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Library/Product_Order.thy
--- a/src/HOL/Library/Product_Order.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Library/Product_Order.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -161,7 +161,7 @@
 instantiation prod :: (Inf, Inf) Inf
 begin
 
-definition "Inf A = (INF x:A. fst x, INF x:A. snd x)"
+definition "Inf A = (INF x\<in>A. fst x, INF x\<in>A. snd x)"
 
 instance ..
 
@@ -170,7 +170,7 @@
 instantiation prod :: (Sup, Sup) Sup
 begin
 
-definition "Sup A = (SUP x:A. fst x, SUP x:A. snd x)"
+definition "Sup A = (SUP x\<in>A. fst x, SUP x\<in>A. snd x)"
 
 instance ..
 
@@ -185,34 +185,34 @@
   by standard (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
     INF_lower SUP_upper le_INF_iff SUP_le_iff bot_prod_def top_prod_def)
 
-lemma fst_Sup: "fst (Sup A) = (SUP x:A. fst x)"
+lemma fst_Sup: "fst (Sup A) = (SUP x\<in>A. fst x)"
   unfolding Sup_prod_def by simp
 
-lemma snd_Sup: "snd (Sup A) = (SUP x:A. snd x)"
+lemma snd_Sup: "snd (Sup A) = (SUP x\<in>A. snd x)"
   unfolding Sup_prod_def by simp
 
-lemma fst_Inf: "fst (Inf A) = (INF x:A. fst x)"
+lemma fst_Inf: "fst (Inf A) = (INF x\<in>A. fst x)"
   unfolding Inf_prod_def by simp
 
-lemma snd_Inf: "snd (Inf A) = (INF x:A. snd x)"
+lemma snd_Inf: "snd (Inf A) = (INF x\<in>A. snd x)"
   unfolding Inf_prod_def by simp
 
-lemma fst_SUP: "fst (SUP x:A. f x) = (SUP x:A. fst (f x))"
+lemma fst_SUP: "fst (SUP x\<in>A. f x) = (SUP x\<in>A. fst (f x))"
   using fst_Sup [of "f ` A", symmetric] by (simp add: comp_def)
 
-lemma snd_SUP: "snd (SUP x:A. f x) = (SUP x:A. snd (f x))"
+lemma snd_SUP: "snd (SUP x\<in>A. f x) = (SUP x\<in>A. snd (f x))"
   using snd_Sup [of "f ` A", symmetric] by (simp add: comp_def)
 
-lemma fst_INF: "fst (INF x:A. f x) = (INF x:A. fst (f x))"
+lemma fst_INF: "fst (INF x\<in>A. f x) = (INF x\<in>A. fst (f x))"
   using fst_Inf [of "f ` A", symmetric] by (simp add: comp_def)
 
-lemma snd_INF: "snd (INF x:A. f x) = (INF x:A. snd (f x))"
+lemma snd_INF: "snd (INF x\<in>A. f x) = (INF x\<in>A. snd (f x))"
   using snd_Inf [of "f ` A", symmetric] by (simp add: comp_def)
 
-lemma SUP_Pair: "(SUP x:A. (f x, g x)) = (SUP x:A. f x, SUP x:A. g x)"
+lemma SUP_Pair: "(SUP x\<in>A. (f x, g x)) = (SUP x\<in>A. f x, SUP x\<in>A. g x)"
   unfolding Sup_prod_def by (simp add: comp_def)
 
-lemma INF_Pair: "(INF x:A. (f x, g x)) = (INF x:A. f x, INF x:A. g x)"
+lemma INF_Pair: "(INF x\<in>A. (f x, g x)) = (INF x\<in>A. f x, INF x\<in>A. g x)"
   unfolding Inf_prod_def by (simp add: comp_def)
 
 
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Probability/Discrete_Topology.thy
--- a/src/HOL/Probability/Discrete_Topology.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Probability/Discrete_Topology.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -19,7 +19,7 @@
   where "dist_discrete n m = (if n = m then 0 else 1)"
 
 definition uniformity_discrete :: "('a discrete \<times> 'a discrete) filter" where
-  "(uniformity::('a discrete \<times> 'a discrete) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+  "(uniformity::('a discrete \<times> 'a discrete) filter) = (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})"
 
 definition "open_discrete" :: "'a discrete set \<Rightarrow> bool" where
   "(open::'a discrete set \<Rightarrow> bool) U \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Probability/Distribution_Functions.thy
--- a/src/HOL/Probability/Distribution_Functions.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Probability/Distribution_Functions.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -220,13 +220,13 @@
     and finite_borel_measure_interval_measure: "finite_borel_measure (interval_measure F)"
 proof -
   let ?F = "interval_measure F"
-  { have "ennreal (m - 0) = (SUP i::nat. ennreal (F (real i) - F (- real i)))"
+  { have "ennreal (m - 0) = (SUP i. ennreal (F (real i) - F (- real i)))"
       by (intro LIMSEQ_unique[OF _ LIMSEQ_SUP] tendsto_ennrealI tendsto_intros
                 lim_F_at_bot[THEN filterlim_compose] lim_F_at_top[THEN filterlim_compose]
                 lim_F_at_bot[THEN filterlim_compose] filterlim_real_sequentially
                 filterlim_uminus_at_top[THEN iffD1])
          (auto simp: incseq_def nondecF intro!: diff_mono)
-    also have "\<dots> = (SUP i::nat. emeasure ?F {- real i<..real i})"
+    also have "\<dots> = (SUP i. emeasure ?F {- real i<..real i})"
       by (subst emeasure_interval_measure_Ioc) (simp_all add: nondecF right_cont_F)
     also have "\<dots> = emeasure ?F (\<Union>i::nat. {- real i<..real i})"
       by (rule SUP_emeasure_incseq) (auto simp: incseq_def)
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Probability/Essential_Supremum.thy
--- a/src/HOL/Probability/Essential_Supremum.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Probability/Essential_Supremum.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -30,13 +30,13 @@
   fix y assume "AE x in M. f x \<le> y"
   then have "(\<lambda>x. f x \<le> y) \<in> {P. AE x in M. P x}"
     by simp
-  then show "(INF P:{P. AE x in M. P x}. SUP x:Collect P. f x) \<le> y"
+  then show "(INF P\<in>{P. AE x in M. P x}. SUP x\<in>Collect P. f x) \<le> y"
     by (rule INF_lower2) (auto intro: SUP_least)
 next
   fix P assume P: "AE x in M. P x"
-  show "Inf {z. AE x in M. f x \<le> z} \<le> (SUP x:Collect P. f x)"
+  show "Inf {z. AE x in M. f x \<le> z} \<le> (SUP x\<in>Collect P. f x)"
   proof (rule Inf_lower; clarsimp)
-    show "AE x in M. f x \<le> (SUP x:Collect P. f x)"
+    show "AE x in M. f x \<le> (SUP x\<in>Collect P. f x)"
       using P by (auto elim: eventually_mono simp: SUP_upper)
   qed
 qed
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Probability/Fin_Map.thy
--- a/src/HOL/Probability/Fin_Map.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Probability/Fin_Map.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -258,7 +258,7 @@
 
 definition [code del]:
   "(uniformity :: (('a, 'b) fmap \<times> ('a \<Rightarrow>\<^sub>F 'b)) filter) =
-    (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+    (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})"
 
 instance
   by standard (rule uniformity_fmap_def)
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Probability/Giry_Monad.thy
--- a/src/HOL/Probability/Giry_Monad.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Probability/Giry_Monad.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -165,7 +165,7 @@
 
 definition subprob_algebra :: "'a measure \<Rightarrow> 'a measure measure" where
   "subprob_algebra K =
-    (SUP A : sets K. vimage_algebra {M. subprob_space M \<and> sets M = sets K} (\<lambda>M. emeasure M A) borel)"
+    (SUP A \<in> sets K. vimage_algebra {M. subprob_space M \<and> sets M = sets K} (\<lambda>M. emeasure M A) borel)"
 
 lemma space_subprob_algebra: "space (subprob_algebra A) = {M. subprob_space M \<and> sets M = sets A}"
   by (auto simp add: subprob_algebra_def space_Sup_eq_UN)
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Probability/Helly_Selection.thy
--- a/src/HOL/Probability/Helly_Selection.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Probability/Helly_Selection.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -87,7 +87,7 @@
     by auto
 
   define F where "F x = Inf {lim (?f n) |n. x < r n}" for x
-  have F_eq: "ereal (F x) = (INF n:{n. x < r n}. ereal (lim (?f n)))" for x
+  have F_eq: "ereal (F x) = (INF n\<in>{n. x < r n}. ereal (lim (?f n)))" for x
     unfolding F_def by (subst ereal_Inf'[OF bdd_below nonempty]) (simp add: setcompr_eq_image)
   have mono_F: "mono F"
     using nonempty by (auto intro!: cInf_superset_mono simp: F_def bdd_below mono_def)
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Probability/Projective_Family.thy
--- a/src/HOL/Probability/Projective_Family.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Probability/Projective_Family.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -470,7 +470,7 @@
     next
       assume *: "{i. J i \<subseteq> {0..< n}} \<noteq> {}"
       have "(INF i. CI (J i) (X' i)) \<le>
-          (INF i:{i. J i \<subseteq> {0..<n}}. C 0 n (\<lambda>_. undefined) (PF.emb {0..<n} (J i) (X' i)))"
+          (INF i\<in>{i. J i \<subseteq> {0..<n}}. C 0 n (\<lambda>_. undefined) (PF.emb {0..<n} (J i) (X' i)))"
         by (intro INF_superset_mono) (auto simp: emeasure_CI)
       also have "\<dots> = C 0 n (\<lambda>_. undefined) (\<Inter>i\<in>{i. J i \<subseteq> {0..<n}}. (PF.emb {0..<n} (J i) (X' i)))"
         using * by (intro emeasure_INT_decseq_subset[symmetric]) (auto intro!: dec_X' del: subsetI simp: sets_C)
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Probability/Projective_Limit.thy
--- a/src/HOL/Probability/Projective_Limit.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Probability/Projective_Limit.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -141,7 +141,7 @@
     unfolding P'_def mapmeasure_def using J
     by (auto intro!: prob_space_distr fm_measurable simp: measurable_cong_sets[OF sets_P])
 
-  let ?SUP = "\<lambda>n. SUP K : {K. K \<subseteq> fm n ` (B n) \<and> compact K}. emeasure (P' n) K"
+  let ?SUP = "\<lambda>n. SUP K \<in> {K. K \<subseteq> fm n ` (B n) \<and> compact K}. emeasure (P' n) K"
   { fix n
     have "emeasure (P (J n)) (B n) = emeasure (P' n) (fm n ` (B n))"
       using J by (auto simp: P'_def mapmeasure_PiM space_P sets_P)
@@ -169,7 +169,7 @@
       have "?SUP n + 0 < ?SUP n + 2 powr (-n) * ?a"
         using R[of n] unfolding ennreal_add_left_cancel_less ennreal_zero_less_mult_iff
         by (auto intro: \<open>0 < ?a\<close>)
-      also have "\<dots> = (SUP K:{K. K \<subseteq> fm n ` B n \<and> compact K}. emeasure (P' n) K + 2 powr (-n) * ?a)"
+      also have "\<dots> = (SUP K\<in>{K. K \<subseteq> fm n ` B n \<and> compact K}. emeasure (P' n) K + 2 powr (-n) * ?a)"
         by (rule ennreal_SUP_add_left[symmetric]) auto
       also have "\<dots> \<le> ?SUP n"
       proof (intro SUP_least)
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Probability/SPMF.thy
--- a/src/HOL/Probability/SPMF.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Probability/SPMF.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -10,7 +10,7 @@
 
 subsection \<open>Auxiliary material\<close>
 
-lemma cSUP_singleton [simp]: "(SUP x:{x}. f x :: _ :: conditionally_complete_lattice) = f x"
+lemma cSUP_singleton [simp]: "(SUP x\<in>{x}. f x :: _ :: conditionally_complete_lattice) = f x"
 by (metis cSup_singleton image_empty image_insert)
 
 subsubsection \<open>More about extended reals\<close>
@@ -33,18 +33,18 @@
   unfolding continuous_def by auto
 
 lemma ennreal_Sup:
-  assumes *: "(SUP a:A. ennreal a) \<noteq> \<top>"
+  assumes *: "(SUP a\<in>A. ennreal a) \<noteq> \<top>"
   and "A \<noteq> {}"
-  shows "ennreal (Sup A) = (SUP a:A. ennreal a)"
+  shows "ennreal (Sup A) = (SUP a\<in>A. ennreal a)"
 proof (rule continuous_at_Sup_mono)
-  obtain r where r: "ennreal r = (SUP a:A. ennreal a)" "r \<ge> 0"
-    using * by(cases "(SUP a:A. ennreal a)") simp_all
+  obtain r where r: "ennreal r = (SUP a\<in>A. ennreal a)" "r \<ge> 0"
+    using * by(cases "(SUP a\<in>A. ennreal a)") simp_all
   then show "bdd_above A"
     by(auto intro!: SUP_upper bdd_aboveI[of _ r] simp add: ennreal_le_iff[symmetric])
 qed (auto simp: mono_def continuous_at_imp_continuous_at_within continuous_at_ennreal ennreal_leI assms)
 
 lemma ennreal_SUP:
-  "\<lbrakk> (SUP a:A. ennreal (f a)) \<noteq> \<top>; A \<noteq> {} \<rbrakk> \<Longrightarrow> ennreal (SUP a:A. f a) = (SUP a:A. ennreal (f a))"
+  "\<lbrakk> (SUP a\<in>A. ennreal (f a)) \<noteq> \<top>; A \<noteq> {} \<rbrakk> \<Longrightarrow> ennreal (SUP a\<in>A. f a) = (SUP a\<in>A. ennreal (f a))"
 using ennreal_Sup[of "f ` A"] by auto
 
 lemma ennreal_lt_0: "x < 0 \<Longrightarrow> ennreal x = 0"
@@ -333,9 +333,9 @@
 lemma nn_integral_spmf_neq_top: "(\<integral>\<^sup>+ x. spmf p x \<partial>count_space UNIV) \<noteq> \<top>"
 using nn_integral_measure_spmf[where f="\<lambda>_. 1", of p, symmetric] by simp
 
-lemma SUP_spmf_neq_top': "(SUP p:Y. ennreal (spmf p x)) \<noteq> \<top>"
+lemma SUP_spmf_neq_top': "(SUP p\<in>Y. ennreal (spmf p x)) \<noteq> \<top>"
 proof(rule neq_top_trans)
-  show "(SUP p:Y. ennreal (spmf p x)) \<le> 1" by(rule SUP_least)(simp add: pmf_le_1)
+  show "(SUP p\<in>Y. ennreal (spmf p x)) \<le> 1" by(rule SUP_least)(simp add: pmf_le_1)
 qed simp
 
 lemma SUP_spmf_neq_top: "(SUP i. ennreal (spmf (Y i) x)) \<noteq> \<top>"
@@ -343,9 +343,9 @@
   show "(SUP i. ennreal (spmf (Y i) x)) \<le> 1" by(rule SUP_least)(simp add: pmf_le_1)
 qed simp
 
-lemma SUP_emeasure_spmf_neq_top: "(SUP p:Y. emeasure (measure_spmf p) A) \<noteq> \<top>"
+lemma SUP_emeasure_spmf_neq_top: "(SUP p\<in>Y. emeasure (measure_spmf p) A) \<noteq> \<top>"
 proof(rule neq_top_trans)
-  show "(SUP p:Y. emeasure (measure_spmf p) A) \<le> 1"
+  show "(SUP p\<in>Y. emeasure (measure_spmf p) A) \<le> 1"
     by(rule SUP_least)(simp add: measure_spmf.subprob_emeasure_le_1)
 qed simp
 
@@ -1228,7 +1228,7 @@
 context fixes Y :: "'a spmf set" begin
 
 definition lub_spmf :: "'a spmf"
-where "lub_spmf = embed_spmf (\<lambda>x. enn2real (SUP p : Y. ennreal (spmf p x)))"
+where "lub_spmf = embed_spmf (\<lambda>x. enn2real (SUP p \<in> Y. ennreal (spmf p x)))"
   \<comment> \<open>We go through @{typ ennreal} to have a sensible definition even if @{term Y} is empty.\<close>
 
 lemma lub_spmf_empty [simp]: "SPMF.lub_spmf {} = return_pmf None"
@@ -1339,7 +1339,7 @@
   qed
 qed simp
 
-lemma lub_spmf_subprob: "(\<integral>\<^sup>+ x. (SUP p : Y. ennreal (spmf p x)) \<partial>count_space UNIV) \<le> 1"
+lemma lub_spmf_subprob: "(\<integral>\<^sup>+ x. (SUP p \<in> Y. ennreal (spmf p x)) \<partial>count_space UNIV) \<le> 1"
 proof(cases "Y = {}")
   case True
   thus ?thesis by(simp add: bot_ennreal)
@@ -1348,13 +1348,13 @@
   let ?B = "\<Union>p\<in>Y. set_spmf p"
   have countable: "countable ?B" by(rule spmf_chain_countable)
 
-  have "(\<integral>\<^sup>+ x. (SUP p:Y. ennreal (spmf p x)) \<partial>count_space UNIV) =
-        (\<integral>\<^sup>+ x. (SUP p:Y. ennreal (spmf p x) * indicator ?B x) \<partial>count_space UNIV)"
+  have "(\<integral>\<^sup>+ x. (SUP p\<in>Y. ennreal (spmf p x)) \<partial>count_space UNIV) =
+        (\<integral>\<^sup>+ x. (SUP p\<in>Y. ennreal (spmf p x) * indicator ?B x) \<partial>count_space UNIV)"
     by(intro nn_integral_cong SUP_cong)(auto split: split_indicator simp add: spmf_eq_0_set_spmf)
-  also have "\<dots> = (\<integral>\<^sup>+ x. (SUP p:Y. ennreal (spmf p x)) \<partial>count_space ?B)"
+  also have "\<dots> = (\<integral>\<^sup>+ x. (SUP p\<in>Y. ennreal (spmf p x)) \<partial>count_space ?B)"
     unfolding ennreal_indicator[symmetric] using False
     by(subst SUP_mult_right_ennreal[symmetric])(simp add: ennreal_indicator nn_integral_count_space_indicator)
-  also have "\<dots> = (SUP p:Y. \<integral>\<^sup>+ x. spmf p x \<partial>count_space ?B)" using False _ countable
+  also have "\<dots> = (SUP p\<in>Y. \<integral>\<^sup>+ x. spmf p x \<partial>count_space ?B)" using False _ countable
     by(rule nn_integral_monotone_convergence_SUP_countable)(rule chain_ord_spmf_eqD)
   also have "\<dots> \<le> 1"
   proof(rule SUP_least)
@@ -1373,23 +1373,23 @@
 
 lemma spmf_lub_spmf:
   assumes "Y \<noteq> {}"
-  shows "spmf lub_spmf x = (SUP p : Y. spmf p x)"
+  shows "spmf lub_spmf x = (SUP p \<in> Y. spmf p x)"
 proof -
   from assms obtain p where "p \<in> Y" by auto
-  have "spmf lub_spmf x = max 0 (enn2real (SUP p:Y. ennreal (spmf p x)))" unfolding lub_spmf_def
+  have "spmf lub_spmf x = max 0 (enn2real (SUP p\<in>Y. ennreal (spmf p x)))" unfolding lub_spmf_def
     by(rule spmf_embed_spmf)(simp del: SUP_eq_top_iff Sup_eq_top_iff add: ennreal_enn2real_if SUP_spmf_neq_top' lub_spmf_subprob)
-  also have "\<dots> = enn2real (SUP p:Y. ennreal (spmf p x))"
+  also have "\<dots> = enn2real (SUP p\<in>Y. ennreal (spmf p x))"
     by(rule max_absorb2)(simp)
-  also have "\<dots> = enn2real (ennreal (SUP p : Y. spmf p x))" using assms
+  also have "\<dots> = enn2real (ennreal (SUP p \<in> Y. spmf p x))" using assms
     by(subst ennreal_SUP[symmetric])(simp_all add: SUP_spmf_neq_top' del: SUP_eq_top_iff Sup_eq_top_iff)
   also have "0 \<le> (\<Squnion>p\<in>Y. spmf p x)" using assms
     by(auto intro!: cSUP_upper2 bdd_aboveI[where M=1] simp add: pmf_le_1)
-  then have "enn2real (ennreal (SUP p : Y. spmf p x)) = (SUP p : Y. spmf p x)"
+  then have "enn2real (ennreal (SUP p \<in> Y. spmf p x)) = (SUP p \<in> Y. spmf p x)"
     by(rule enn2real_ennreal)
   finally show ?thesis .
 qed
 
-lemma ennreal_spmf_lub_spmf: "Y \<noteq> {} \<Longrightarrow> ennreal (spmf lub_spmf x) = (SUP p:Y. ennreal (spmf p x))"
+lemma ennreal_spmf_lub_spmf: "Y \<noteq> {} \<Longrightarrow> ennreal (spmf lub_spmf x) = (SUP p\<in>Y. ennreal (spmf p x))"
 unfolding spmf_lub_spmf by(subst ennreal_SUP)(simp_all add: SUP_spmf_neq_top' del: SUP_eq_top_iff Sup_eq_top_iff)
 
 lemma lub_spmf_upper:
@@ -1398,7 +1398,7 @@
 proof(rule ord_pmf_increaseI)
   fix x
   from p have [simp]: "Y \<noteq> {}" by auto
-  from p have "ennreal (spmf p x) \<le> (SUP p:Y. ennreal (spmf p x))" by(rule SUP_upper)
+  from p have "ennreal (spmf p x) \<le> (SUP p\<in>Y. ennreal (spmf p x))" by(rule SUP_upper)
   also have "\<dots> = ennreal (spmf lub_spmf x)" using p
     by(subst spmf_lub_spmf)(auto simp add: ennreal_SUP SUP_spmf_neq_top' simp del: SUP_eq_top_iff Sup_eq_top_iff)
   finally show "spmf p x \<le> spmf lub_spmf x" by simp
@@ -1413,7 +1413,7 @@
   proof(rule ord_pmf_increaseI)
     fix x
     from nonempty obtain p where p: "p \<in> Y" by auto
-    have "ennreal (spmf lub_spmf x) = (SUP p:Y. ennreal (spmf p x))"
+    have "ennreal (spmf lub_spmf x) = (SUP p\<in>Y. ennreal (spmf p x))"
       by(subst spmf_lub_spmf)(auto simp add: ennreal_SUP SUP_spmf_neq_top' nonempty simp del: SUP_eq_top_iff Sup_eq_top_iff)
     also have "\<dots> \<le> ennreal (spmf z x)" by(rule SUP_least)(simp add: ord_spmf_eq_leD z)
     finally show "spmf lub_spmf x \<le> spmf z x" by simp
@@ -1438,16 +1438,16 @@
 
 lemma emeasure_lub_spmf:
   assumes Y: "Y \<noteq> {}"
-  shows "emeasure (measure_spmf lub_spmf) A = (SUP y:Y. emeasure (measure_spmf y) A)"
+  shows "emeasure (measure_spmf lub_spmf) A = (SUP y\<in>Y. emeasure (measure_spmf y) A)"
   (is "?lhs = ?rhs")
 proof -
   let ?M = "count_space (set_spmf lub_spmf)"
   have "?lhs = \<integral>\<^sup>+ x. ennreal (spmf lub_spmf x) * indicator A x \<partial>?M"
     by(auto simp add: nn_integral_indicator[symmetric] nn_integral_measure_spmf')
-  also have "\<dots> = \<integral>\<^sup>+ x. (SUP y:Y. ennreal (spmf y x) * indicator A x) \<partial>?M"
+  also have "\<dots> = \<integral>\<^sup>+ x. (SUP y\<in>Y. ennreal (spmf y x) * indicator A x) \<partial>?M"
     unfolding ennreal_indicator[symmetric]
     by(simp add: spmf_lub_spmf assms ennreal_SUP[OF SUP_spmf_neq_top'] SUP_mult_right_ennreal)
-  also from assms have "\<dots> = (SUP y:Y. \<integral>\<^sup>+ x. ennreal (spmf y x) * indicator A x \<partial>?M)"
+  also from assms have "\<dots> = (SUP y\<in>Y. \<integral>\<^sup>+ x. ennreal (spmf y x) * indicator A x \<partial>?M)"
   proof(rule nn_integral_monotone_convergence_SUP_countable)
     have "(\<lambda>i x. ennreal (spmf i x) * indicator A x) ` Y = (\<lambda>f x. f x * indicator A x) ` (\<lambda>p x. ennreal (spmf p x)) ` Y"
       by(simp add: image_image)
@@ -1455,7 +1455,7 @@
       by(rule chain_imageI)(auto simp add: le_fun_def split: split_indicator)
     finally show "Complete_Partial_Order.chain (\<le>) ((\<lambda>i x. ennreal (spmf i x) * indicator A x) ` Y)" .
   qed simp
-  also have "\<dots> = (SUP y:Y. \<integral>\<^sup>+ x. ennreal (spmf y x) * indicator A x \<partial>count_space UNIV)"
+  also have "\<dots> = (SUP y\<in>Y. \<integral>\<^sup>+ x. ennreal (spmf y x) * indicator A x \<partial>count_space UNIV)"
     by(auto simp add: nn_integral_count_space_indicator set_lub_spmf spmf_eq_0_set_spmf split: split_indicator intro!: SUP_cong nn_integral_cong)
   also have "\<dots> = ?rhs"
     by(auto simp add: nn_integral_indicator[symmetric] nn_integral_measure_spmf)
@@ -1464,7 +1464,7 @@
 
 lemma measure_lub_spmf:
   assumes Y: "Y \<noteq> {}"
-  shows "measure (measure_spmf lub_spmf) A = (SUP y:Y. measure (measure_spmf y) A)" (is "?lhs = ?rhs")
+  shows "measure (measure_spmf lub_spmf) A = (SUP y\<in>Y. measure (measure_spmf y) A)" (is "?lhs = ?rhs")
 proof -
   have "ennreal ?lhs = ennreal ?rhs"
     using emeasure_lub_spmf[OF assms] SUP_emeasure_spmf_neq_top[of A Y] Y
@@ -1476,12 +1476,12 @@
 
 lemma weight_lub_spmf:
   assumes Y: "Y \<noteq> {}"
-  shows "weight_spmf lub_spmf = (SUP y:Y. weight_spmf y)"
+  shows "weight_spmf lub_spmf = (SUP y\<in>Y. weight_spmf y)"
 unfolding weight_spmf_def by(rule measure_lub_spmf) fact
 
 lemma measure_spmf_lub_spmf:
   assumes Y: "Y \<noteq> {}"
-  shows "measure_spmf lub_spmf = (SUP p:Y. measure_spmf p)" (is "?lhs = ?rhs")
+  shows "measure_spmf lub_spmf = (SUP p\<in>Y. measure_spmf p)" (is "?lhs = ?rhs")
 proof(rule measure_eqI)
   from assms obtain p where p: "p \<in> Y" by auto
   from chain have chain': "Complete_Partial_Order.chain (\<le>) (measure_spmf ` Y)"
@@ -1583,11 +1583,11 @@
     let ?M = "count_space (set_spmf (lub_spmf Y))"
     have "ennreal (spmf ?lhs i) = \<integral>\<^sup>+ x. ennreal (spmf (lub_spmf Y) x) * ennreal (spmf (f x) i) \<partial>?M"
       by(auto simp add: ennreal_spmf_lub_spmf ennreal_spmf_bind nn_integral_measure_spmf')
-    also have "\<dots> = \<integral>\<^sup>+ x. (SUP p:Y. ennreal (spmf p x * spmf (f x) i)) \<partial>?M"
+    also have "\<dots> = \<integral>\<^sup>+ x. (SUP p\<in>Y. ennreal (spmf p x * spmf (f x) i)) \<partial>?M"
       by(subst ennreal_spmf_lub_spmf[OF chain Y])(subst SUP_mult_right_ennreal, simp_all add: ennreal_mult Y)
-    also have "\<dots> = (SUP p:Y. \<integral>\<^sup>+ x. ennreal (spmf p x * spmf (f x) i) \<partial>?M)"
+    also have "\<dots> = (SUP p\<in>Y. \<integral>\<^sup>+ x. ennreal (spmf p x * spmf (f x) i) \<partial>?M)"
       using Y chain' by(rule nn_integral_monotone_convergence_SUP_countable) simp
-    also have "\<dots> = (SUP p:Y. ennreal (spmf (bind_spmf p f) i))"
+    also have "\<dots> = (SUP p\<in>Y. ennreal (spmf (bind_spmf p f) i))"
       by(auto simp add: ennreal_spmf_bind nn_integral_measure_spmf nn_integral_count_space_indicator set_lub_spmf[OF chain] in_set_spmf_iff_spmf ennreal_mult intro!: SUP_cong nn_integral_cong split: split_indicator)
     also have "\<dots> = ennreal (spmf ?rhs i)" using chain'' by(simp add: ennreal_spmf_lub_spmf Y)
     finally show "spmf ?lhs i = spmf ?rhs i" by simp
@@ -1619,12 +1619,12 @@
     have chain''': "Complete_Partial_Order.chain (ord_spmf (=)) ((\<lambda>p. bind_spmf x (\<lambda>y. g y p)) ` Y)"
       using chain by(rule chain_imageI)(rule monotone_bind_spmf2[OF g, THEN monotoneD])
 
-    have "ennreal (spmf ?lhs i) = \<integral>\<^sup>+ y. (SUP p:Y. ennreal (spmf x y * spmf (g y p) i)) \<partial>count_space (set_spmf x)"
+    have "ennreal (spmf ?lhs i) = \<integral>\<^sup>+ y. (SUP p\<in>Y. ennreal (spmf x y * spmf (g y p) i)) \<partial>count_space (set_spmf x)"
       by(simp add: ennreal_spmf_bind ennreal_spmf_lub_spmf[OF chain'] Y nn_integral_measure_spmf' SUP_mult_left_ennreal ennreal_mult)
-    also have "\<dots> = (SUP p:Y. \<integral>\<^sup>+ y. ennreal (spmf x y * spmf (g y p) i) \<partial>count_space (set_spmf x))"
+    also have "\<dots> = (SUP p\<in>Y. \<integral>\<^sup>+ y. ennreal (spmf x y * spmf (g y p) i) \<partial>count_space (set_spmf x))"
       unfolding nn_integral_measure_spmf' using Y chain''
       by(rule nn_integral_monotone_convergence_SUP_countable) simp
-    also have "\<dots> = (SUP p:Y. ennreal (spmf (bind_spmf x (\<lambda>y. g y p)) i))"
+    also have "\<dots> = (SUP p\<in>Y. ennreal (spmf (bind_spmf x (\<lambda>y. g y p)) i))"
       by(simp add: ennreal_spmf_bind nn_integral_measure_spmf' ennreal_mult)
     also have "\<dots> = ennreal (spmf ?rhs i)" using chain'''
       by(auto simp add: ennreal_spmf_lub_spmf Y)
@@ -1775,9 +1775,9 @@
       by(auto simp add: weight_lub_spmf chain1 chain2 Y rel_spmf_weightD[OF R, symmetric] intro!: cSUP_least intro: cSUP_upper2[OF bdd_aboveI2[OF weight_spmf_le_1]])
 
     fix A
-    have "measure (measure_spmf (lub_spmf (fst ` Y))) A = (SUP y:fst ` Y. measure (measure_spmf y) A)"
+    have "measure (measure_spmf (lub_spmf (fst ` Y))) A = (SUP y\<in>fst ` Y. measure (measure_spmf y) A)"
       using chain1 Y1 by(rule measure_lub_spmf)
-    also have "\<dots> \<le> (SUP y:snd ` Y. measure (measure_spmf y) {y. \<exists>x\<in>A. R x y})" using Y1
+    also have "\<dots> \<le> (SUP y\<in>snd ` Y. measure (measure_spmf y) {y. \<exists>x\<in>A. R x y})" using Y1
       by(rule cSUP_least)(auto intro!: cSUP_upper2[OF bdd_aboveI2[OF measure_spmf.subprob_measure_le_1]] rel_spmf_measureD R)
     also have "\<dots> = measure (measure_spmf (lub_spmf (snd ` Y))) {y. \<exists>x\<in>A. R x y}"
       using chain2 Y2 by(rule measure_lub_spmf[symmetric])
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Probability/Stream_Space.thy
--- a/src/HOL/Probability/Stream_Space.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Probability/Stream_Space.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -279,7 +279,7 @@
            simp add: sets_PiM_eq_proj snth_in space sets cong: measurable_cong_sets)
 
 lemma sets_stream_space_eq: "sets (stream_space M) =
-    sets (SUP i:UNIV. vimage_algebra (streams (space M)) (\<lambda>s. s !! i) M)"
+    sets (SUP i\<in>UNIV. vimage_algebra (streams (space M)) (\<lambda>s. s !! i) M)"
   by (auto intro!: sets_stream_space_in_sets sets_Sup_in_sets sets_image_in_sets
                    measurable_Sup1 snth_in measurable_vimage_algebra1 del: subsetI
            simp: space_Sup_eq_UN space_stream_space)
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Probability/Weak_Convergence.thy
--- a/src/HOL/Probability/Weak_Convergence.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Probability/Weak_Convergence.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -53,7 +53,7 @@
     by (auto intro!: cInf_lower bdd)
 
   { assume *: "I \<omega> \<le> x"
-    have "\<omega> \<le> (INF s:{x. \<omega> \<le> f x}. f s)"
+    have "\<omega> \<le> (INF s\<in>{x. \<omega> \<le> f x}. f s)"
       by (rule cINF_greatest[OF ne]) auto
     also have "\<dots> = f (I \<omega>)"
       using continuous_at_Inf_mono[OF mono cont ne bdd] ..
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -597,7 +597,7 @@
   assumes dist_norm: "dist x y = norm (x - y)"
 
 class uniformity_dist = dist + uniformity +
-  assumes uniformity_dist: "uniformity = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+  assumes uniformity_dist: "uniformity = (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})"
 begin
 
 lemma eventually_uniformity_metric:
@@ -1133,7 +1133,7 @@
 definition dist_real_def: "dist x y = \<bar>x - y\<bar>"
 
 definition uniformity_real_def [code del]:
-  "(uniformity :: (real \<times> real) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+  "(uniformity :: (real \<times> real) filter) = (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})"
 
 definition open_real_def [code del]:
   "open (U :: real set) \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
@@ -1611,7 +1611,7 @@
 
 subsection \<open>Filters and Limits on Metric Space\<close>
 
-lemma (in metric_space) nhds_metric: "nhds x = (INF e:{0 <..}. principal {y. dist y x < e})"
+lemma (in metric_space) nhds_metric: "nhds x = (INF e\<in>{0 <..}. principal {y. dist y x < e})"
   unfolding nhds_def
 proof (safe intro!: INF_eq)
   fix S
diff -r 438e1a11445f -r 0a9688695a1b src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Topological_Spaces.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -517,7 +517,7 @@
   by (auto simp: nhds_discrete filterlim_principal)
 
 lemma (in topological_space) at_within_eq:
-  "at x within s = (INF S:{S. open S \<and> x \<in> S}. principal (S \<inter> s - {x}))"
+  "at x within s = (INF S\<in>{S. open S \<and> x \<in> S}. principal (S \<inter> s - {x}))"
   unfolding nhds_def at_within_def
   by (subst INF_inf_const2[symmetric]) (auto simp: Diff_Int_distrib)
 
@@ -575,7 +575,7 @@
   by (simp add: at_eq_bot_iff not_open_singleton)
 
 lemma (in order_topology) nhds_order:
-  "nhds x = inf (INF a:{x <..}. principal {..< a}) (INF a:{..< x}. principal {a <..})"
+  "nhds x = inf (INF a\<in>{x <..}. principal {..< a}) (INF a\<in>{..< x}. principal {a <..})"
 proof -
   have 1: "{S \<in> range lessThan \<union> range greaterThan. x \<in> S} =
       (\<lambda>a. {..< a}) ` {x <..} \<union> (\<lambda>a. {a <..}) ` {..< x}"
@@ -616,8 +616,8 @@
 lemma (in linorder_topology) at_within_order:
   assumes "UNIV \<noteq> {x}"
   shows "at x within s =
-    inf (INF a:{x <..}. principal ({..< a} \<inter> s - {x}))
-        (INF a:{..< x}. principal ({a <..} \<inter> s - {x}))"
+    inf (INF a\<in>{x <..}. principal ({..< a} \<inter> s - {x}))
+        (INF a\<in>{..< x}. principal ({a <..} \<inter> s - {x}))"
 proof (cases "{x <..} = {}" "{..< x} = {}" rule: case_split [case_product case_split])
   case True_True
   have "UNIV = {..< x} \<union> {x} \<union> {x <..}"
@@ -628,7 +628,7 @@
       inf_principal[symmetric] INF_inf_const2 inf_sup_aci[where 'a="'a filter"])
 
 lemma (in linorder_topology) at_left_eq:
-  "y < x \<Longrightarrow> at_left x = (INF a:{..< x}. principal {a <..< x})"
+  "y < x \<Longrightarrow> at_left x = (INF a\<in>{..< x}. principal {a <..< x})"
   by (subst at_within_order)
      (auto simp: greaterThan_Int_greaterThan greaterThanLessThan_eq[symmetric] min.absorb2 INF_constant
            intro!: INF_lower2 inf_absorb2)
@@ -639,7 +639,7 @@
   by (subst eventually_INF_base) (auto simp: eventually_principal Ball_def)
 
 lemma (in linorder_topology) at_right_eq:
-  "x < y \<Longrightarrow> at_right x = (INF a:{x <..}. principal {x <..< a})"
+  "x < y \<Longrightarrow> at_right x = (INF a\<in>{x <..}. principal {x <..< a})"
   by (subst at_within_order)
      (auto simp: lessThan_Int_lessThan greaterThanLessThan_eq[symmetric] max.absorb2 INF_constant Int_commute
            intro!: INF_lower2 inf_absorb1)
@@ -3039,11 +3039,11 @@
   assumes "mono f"
     and cont: "continuous (at_left (Sup S)) f"
     and S: "S \<noteq> {}" "bdd_above S"
-  shows "f (Sup S) = (SUP s:S. f s)"
+  shows "f (Sup S) = (SUP s\<in>S. f s)"
 proof (rule antisym)
   have f: "(f \<longlongrightarrow> f (Sup S)) (at_left (Sup S))"
     using cont unfolding continuous_within .
-  show "f (Sup S) \<le> (SUP s:S. f s)"
+  show "f (Sup S) \<le> (SUP s\<in>S. f s)"
   proof cases
     assume "Sup S \<in> S"
     then show ?thesis
@@ -3057,8 +3057,8 @@
     show ?thesis
     proof (rule ccontr)
       assume "\<not> ?thesis"
-      with order_tendstoD(1)[OF f, of "SUP s:S. f s"] obtain b where "b < Sup S"
-        and *: "\<And>y. b < y \<Longrightarrow> y < Sup S \<Longrightarrow> (SUP s:S. f s) < f y"
+      with order_tendstoD(1)[OF f, of "SUP s\<in>S. f s"] obtain b where "b < Sup S"
+        and *: "\<And>y. b < y \<Longrightarrow> y < Sup S \<Longrightarrow> (SUP s\<in>S. f s) < f y"
         by (auto simp: not_le eventually_at_left[OF \<open>s < Sup S\<close>])
       with \<open>S \<noteq> {}\<close> obtain c where "c \<in> S" "b < c"
         using less_cSupD[of S b] by auto
@@ -3077,11 +3077,11 @@
   assumes "antimono f"
     and cont: "continuous (at_left (Sup S)) f"
     and S: "S \<noteq> {}" "bdd_above S"
-  shows "f (Sup S) = (INF s:S. f s)"
+  shows "f (Sup S) = (INF s\<in>S. f s)"
 proof (rule antisym)
   have f: "(f \<longlongrightarrow> f (Sup S)) (at_left (Sup S))"
     using cont unfolding continuous_within .
-  show "(INF s:S. f s) \<le> f (Sup S)"
+  show "(INF s\<in>S. f s) \<le> f (Sup S)"
   proof cases
     assume "Sup S \<in> S"
     then show ?thesis
@@ -3095,8 +3095,8 @@
     show ?thesis
     proof (rule ccontr)
       assume "\<not> ?thesis"
-      with order_tendstoD(2)[OF f, of "INF s:S. f s"] obtain b where "b < Sup S"
-        and *: "\<And>y. b < y \<Longrightarrow> y < Sup S \<Longrightarrow> f y < (INF s:S. f s)"
+      with order_tendstoD(2)[OF f, of "INF s\<in>S. f s"] obtain b where "b < Sup S"
+        and *: "\<And>y. b < y \<Longrightarrow> y < Sup S \<Longrightarrow> f y < (INF s\<in>S. f s)"
         by (auto simp: not_le eventually_at_left[OF \<open>s < Sup S\<close>])
       with \<open>S \<noteq> {}\<close> obtain c where "c \<in> S" "b < c"
         using less_cSupD[of S b] by auto
@@ -3115,11 +3115,11 @@
   assumes "mono f"
     and cont: "continuous (at_right (Inf S)) f"
     and S: "S \<noteq> {}" "bdd_below S"
-  shows "f (Inf S) = (INF s:S. f s)"
+  shows "f (Inf S) = (INF s\<in>S. f s)"
 proof (rule antisym)
   have f: "(f \<longlongrightarrow> f (Inf S)) (at_right (Inf S))"
     using cont unfolding continuous_within .
-  show "(INF s:S. f s) \<le> f (Inf S)"
+  show "(INF s\<in>S. f s) \<le> f (Inf S)"
   proof cases
     assume "Inf S \<in> S"
     then show ?thesis
@@ -3133,8 +3133,8 @@
     show ?thesis
     proof (rule ccontr)
       assume "\<not> ?thesis"
-      with order_tendstoD(2)[OF f, of "INF s:S. f s"] obtain b where "Inf S < b"
-        and *: "\<And>y. Inf S < y \<Longrightarrow> y < b \<Longrightarrow> f y < (INF s:S. f s)"
+      with order_tendstoD(2)[OF f, of "INF s\<in>S. f s"] obtain b where "Inf S < b"
+        and *: "\<And>y. Inf S < y \<Longrightarrow> y < b \<Longrightarrow> f y < (INF s\<in>S. f s)"
         by (auto simp: not_le eventually_at_right[OF \<open>Inf S < s\<close>])
       with \<open>S \<noteq> {}\<close> obtain c where "c \<in> S" "c < b"
         using cInf_lessD[of S b] by auto
@@ -3153,11 +3153,11 @@
   assumes "antimono f"
     and cont: "continuous (at_right (Inf S)) f"
     and S: "S \<noteq> {}" "bdd_below S"
-  shows "f (Inf S) = (SUP s:S. f s)"
+  shows "f (Inf S) = (SUP s\<in>S. f s)"
 proof (rule antisym)
   have f: "(f \<longlongrightarrow> f (Inf S)) (at_right (Inf S))"
     using cont unfolding continuous_within .
-  show "f (Inf S) \<le> (SUP s:S. f s)"
+  show "f (Inf S) \<le> (SUP s\<in>S. f s)"
   proof cases
     assume "Inf S \<in> S"
     then show ?thesis
@@ -3171,8 +3171,8 @@
     show ?thesis
     proof (rule ccontr)
       assume "\<not> ?thesis"
-      with order_tendstoD(1)[OF f, of "SUP s:S. f s"] obtain b where "Inf S < b"
-        and *: "\<And>y. Inf S < y \<Longrightarrow> y < b \<Longrightarrow> (SUP s:S. f s) < f y"
+      with order_tendstoD(1)[OF f, of "SUP s\<in>S. f s"] obtain b where "Inf S < b"
+        and *: "\<And>y. Inf S < y \<Longrightarrow> y < b \<Longrightarrow> (SUP s\<in>S. f s) < f y"
         by (auto simp: not_le eventually_at_right[OF \<open>Inf S < s\<close>])
       with \<open>S \<noteq> {}\<close> obtain c where "c \<in> S" "c < b"
         using cInf_lessD[of S b] by auto
@@ -3529,14 +3529,14 @@
 proof (subst prod_filter_INF, auto intro!: antisym INF_greatest simp: principal_prod_principal)
   fix S T
   assume "open S" "a \<in> S" "open T" "b \<in> T"
-  then show "(INF x : {S. open S \<and> (a, b) \<in> S}. principal x) \<le> principal (S \<times> T)"
+  then show "(INF x \<in> {S. open S \<and> (a, b) \<in> S}. principal x) \<le> principal (S \<times> T)"
     by (intro INF_lower) (auto intro!: open_Times)
 next
   fix S'
   assume "open S'" "(a, b) \<in> S'"
   then obtain S T where "open S" "a \<in> S" "open T" "b \<in> T" "S \<times> T \<subseteq> S'"
     by (auto elim: open_prod_elim)
-  then show "(INF x : {S. open S \<and> a \<in> S}. INF y : {S. open S \<and> b \<in> S}.
+  then show "(INF x \<in> {S. open S \<and> a \<in> S}. INF y \<in> {S. open S \<and> b \<in> S}.
       principal (x \<times> y)) \<le> principal S'"
     by (auto intro!: INF_lower2)
 qed