src/HOL/Probability/Regularity.thy
```--- a/src/HOL/Probability/Regularity.thy	Thu Jan 31 11:31:27 2013 +0100
+++ b/src/HOL/Probability/Regularity.thy	Thu Jan 31 11:31:30 2013 +0100
@@ -16,7 +16,7 @@
assumes f_nonneg: "\<And>i. 0 \<le> f i"
assumes approx: "\<And>e. (e::real) > 0 \<Longrightarrow> \<exists>i \<in> A. x \<le> f i + e"
shows "x = (SUP i : A. f i)"
-proof (subst eq_commute, rule ereal_SUPI)
+proof (subst eq_commute, rule SUP_eqI)
show "\<And>i. i \<in> A \<Longrightarrow> f i \<le> x" using f_bound by simp
next
fix y :: ereal assume f_le_y: "(\<And>i::'a. i \<in> A \<Longrightarrow> f i \<le> y)"
@@ -45,7 +45,7 @@
assumes f_nonneg: "\<And>i. 0 \<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)"
-proof (subst eq_commute, rule ereal_INFI)
+proof (subst eq_commute, rule INF_eqI)
show "\<And>i. i \<in> A \<Longrightarrow> x \<le> f i" using f_bound by simp
next
fix y :: ereal assume f_le_y: "(\<And>i::'a. i \<in> A \<Longrightarrow> y \<le> f i)"
@@ -79,7 +79,7 @@
from INF have "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> y \<le> f i) \<Longrightarrow> y \<le> x" by (auto intro: INF_greatest)
ultimately
have "(INF i : A. f i) = x + e" using `e > 0`
-    by (intro ereal_INFI)
+    by (intro INF_eqI)
linorder_not_le not_less_iff_gr_or_eq)
thus False using assms by auto
@@ -97,7 +97,7 @@
from SUP have "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<le> y) \<Longrightarrow> y \<ge> x" by (auto intro: SUP_least)
ultimately
have "(SUP i : A. f i) = x - e" using `e > 0` `\<bar>x\<bar> \<noteq> \<infinity>`
-    by (intro ereal_SUPI)
+    by (intro SUP_eqI)
(metis PInfty_neq_ereal(2) abs_ereal.simps(1) ereal_minus_le linorder_linear,
metis ereal_between(1) ereal_less(2) less_eq_ereal_def order_trans)
thus False using assms by auto
@@ -290,7 +290,7 @@
have "emeasure M A \<le> (INF U:{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!: ereal_INFI)
+    qed (auto intro!: INF_eqI)
note `?inner A` `?outer A` }
note closed_in_D = this
from `B \<in> sets borel`
@@ -299,8 +299,8 @@
then show "?inner B" "?outer B"
proof (induct B rule: sigma_sets_induct_disjoint)
case empty
-    { case 1 show ?case by (intro ereal_SUPI[symmetric]) auto }
-    { case 2 show ?case by (intro ereal_INFI[symmetric]) (auto elim!: meta_allE[of _ "{}"]) }
+    { case 1 show ?case by (intro SUP_eqI[symmetric]) auto }
+    { case 2 show ?case by (intro INF_eqI[symmetric]) (auto elim!: meta_allE[of _ "{}"]) }
next
case (basic B)
{ case 1 from basic closed_in_D show ?case by auto }```