# HG changeset patch
# User haftmann
# Date 1395251242 -3600
# Node ID 1c3f1f2431f909084b6569c92e79b82ecd61f9cd
# Parent  dc429a5b13c497e7f9d63c303fe5068c584b0af3
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION

diff -r dc429a5b13c4 -r 1c3f1f2431f9 NEWS
--- a/NEWS	Wed Mar 19 17:06:02 2014 +0000
+++ b/NEWS	Wed Mar 19 18:47:22 2014 +0100
@@ -98,6 +98,9 @@
 
 *** HOL ***
 
+* Elongated constants INFI and SUPR to INFIMUM and SUPREMUM.
+INCOMPATIBILITY.
+
 * Consolidated theorem names containing INFI and SUPR: have INF
 and SUP instead uniformly.  INCOMPATIBILITY.
 
diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Wed Mar 19 17:06:02 2014 +0000
+++ b/src/HOL/Complete_Lattices.thy	Wed Mar 19 18:47:22 2014 +0100
@@ -17,27 +17,27 @@
   fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
 begin
 
-definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
-  INF_def: "INFI A f = \<Sqinter>(f ` A)"
+definition INFIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
+  INF_def: "INFIMUM A f = \<Sqinter>(f ` A)"
 
 lemma Inf_image_eq [simp]:
-  "\<Sqinter>(f ` A) = INFI A f"
+  "\<Sqinter>(f ` A) = INFIMUM A f"
   by (simp add: INF_def)
 
 lemma INF_image [simp]:
-  "INFI (f ` A) g = INFI A (g \<circ> f)"
+  "INFIMUM (f ` A) g = INFIMUM A (g \<circ> f)"
   by (simp only: INF_def image_comp)
 
 lemma INF_identity_eq [simp]:
-  "INFI A (\<lambda>x. x) = \<Sqinter>A"
+  "INFIMUM A (\<lambda>x. x) = \<Sqinter>A"
   by (simp add: INF_def)
 
 lemma INF_id_eq [simp]:
-  "INFI A id = \<Sqinter>A"
+  "INFIMUM A id = \<Sqinter>A"
   by (simp add: id_def)
 
 lemma INF_cong:
-  "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> INFI A C = INFI B D"
+  "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> INFIMUM A C = INFIMUM B D"
   by (simp add: INF_def image_def)
 
 end
@@ -46,33 +46,33 @@
   fixes Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
 begin
 
-definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
-  SUP_def: "SUPR A f = \<Squnion>(f ` A)"
+definition SUPREMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
+  SUP_def: "SUPREMUM A f = \<Squnion>(f ` A)"
 
 lemma Sup_image_eq [simp]:
-  "\<Squnion>(f ` A) = SUPR A f"
+  "\<Squnion>(f ` A) = SUPREMUM A f"
   by (simp add: SUP_def)
 
 lemma SUP_image [simp]:
-  "SUPR (f ` A) g = SUPR A (g \<circ> f)"
+  "SUPREMUM (f ` A) g = SUPREMUM A (g \<circ> f)"
   by (simp only: SUP_def image_comp)
 
 lemma SUP_identity_eq [simp]:
-  "SUPR A (\<lambda>x. x) = \<Squnion>A"
+  "SUPREMUM A (\<lambda>x. x) = \<Squnion>A"
   by (simp add: SUP_def)
 
 lemma SUP_id_eq [simp]:
-  "SUPR A id = \<Squnion>A"
+  "SUPREMUM A id = \<Squnion>A"
   by (simp add: id_def)
 
 lemma SUP_cong:
-  "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> SUPR A C = SUPR B D"
+  "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> SUPREMUM A C = SUPREMUM B D"
   by (simp add: SUP_def image_def)
 
 end
 
 text {*
-  Note: must use names @{const INFI} and @{const SUPR} here instead of
+  Note: must use names @{const INFIMUM} and @{const SUPREMUM} here instead of
   @{text INF} and @{text SUP} to allow the following syntax coexist
   with the plain constant names.
 *}
@@ -91,17 +91,17 @@
 
 translations
   "INF x y. B"   == "INF x. INF y. B"
-  "INF x. B"     == "CONST INFI CONST UNIV (%x. B)"
+  "INF x. B"     == "CONST INFIMUM CONST UNIV (%x. B)"
   "INF x. B"     == "INF x:CONST UNIV. B"
-  "INF x:A. B"   == "CONST INFI A (%x. B)"
+  "INF x:A. B"   == "CONST INFIMUM A (%x. B)"
   "SUP x y. B"   == "SUP x. SUP y. B"
-  "SUP x. B"     == "CONST SUPR CONST UNIV (%x. B)"
+  "SUP x. B"     == "CONST SUPREMUM CONST UNIV (%x. B)"
   "SUP x. B"     == "SUP x:CONST UNIV. B"
-  "SUP x:A. B"   == "CONST SUPR A (%x. B)"
+  "SUP x:A. B"   == "CONST SUPREMUM A (%x. B)"
 
 print_translation {*
-  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"},
-    Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}]
+  [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFIMUM} @{syntax_const "_INF"},
+    Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPREMUM} @{syntax_const "_SUP"}]
 *} -- {* to avoid eta-contraction of body *}
 
 subsection {* Abstract complete lattices *}
@@ -139,11 +139,11 @@
 begin
 
 lemma INF_foundation_dual:
-  "Sup.SUPR Inf = INFI"
+  "Sup.SUPREMUM Inf = INFIMUM"
   by (simp add: fun_eq_iff Sup.SUP_def)
 
 lemma SUP_foundation_dual:
-  "Inf.INFI Sup = SUPR"
+  "Inf.INFIMUM Sup = SUPREMUM"
   by (simp add: fun_eq_iff Inf.INF_def)
 
 lemma Sup_eqI:
@@ -201,13 +201,13 @@
 lemma Inf_insert [simp]: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
   by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
 
-lemma INF_insert [simp]: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFI A f"
+lemma INF_insert [simp]: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFIMUM A f"
   unfolding INF_def Inf_insert by simp
 
 lemma Sup_insert [simp]: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
   by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
 
-lemma SUP_insert [simp]: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
+lemma SUP_insert [simp]: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPREMUM A f"
   unfolding SUP_def Sup_insert by simp
 
 lemma INF_empty [simp]: "(\<Sqinter>x\<in>{}. f x) = \<top>"
@@ -444,23 +444,23 @@
 lemma Inf_le_Sup: "A \<noteq> {} \<Longrightarrow> Inf A \<le> Sup A"
   by (blast intro: Sup_upper2 Inf_lower ex_in_conv)
 
-lemma INF_le_SUP: "A \<noteq> {} \<Longrightarrow> INFI A f \<le> SUPR A f"
+lemma INF_le_SUP: "A \<noteq> {} \<Longrightarrow> INFIMUM A f \<le> SUPREMUM A f"
   using Inf_le_Sup [of "f ` A"] by simp
 
 lemma SUP_eq_const:
-  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> SUPR I f = x"
+  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> SUPREMUM I f = x"
   by (auto intro: SUP_eqI)
 
 lemma INF_eq_const:
-  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> INFI I f = x"
+  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> INFIMUM I f = x"
   by (auto intro: INF_eqI)
 
 lemma SUP_eq_iff:
-  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> c \<le> f i) \<Longrightarrow> (SUPR I f = c) \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
+  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> c \<le> f i) \<Longrightarrow> (SUPREMUM I f = c) \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
   using SUP_eq_const[of I f c] SUP_upper[of _ I f] by (auto intro: antisym)
 
 lemma INF_eq_iff:
-  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<le> c) \<Longrightarrow> (INFI I f = c) \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
+  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<le> c) \<Longrightarrow> (INFIMUM I f = c) \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
   using INF_eq_const[of I f c] INF_lower[of _ I f] by (auto intro: antisym)
 
 end
@@ -645,7 +645,7 @@
 qed (auto elim!: allE[of _ "\<Sqinter>A"] simp add: not_le[symmetric] Inf_lower)
 
 lemma INF_le_iff:
-  "INFI A f \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)"
+  "INFIMUM A f \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)"
   using Inf_le_iff [of "f ` A"] by simp
 
 lemma le_Sup_iff: "x \<le> \<Squnion>A \<longleftrightarrow> (\<forall>y<x. \<exists>a\<in>A. y < a)"
@@ -656,7 +656,7 @@
     unfolding less_Sup_iff .
 qed (auto elim!: allE[of _ "\<Squnion>A"] simp add: not_le[symmetric] Sup_upper)
 
-lemma le_SUP_iff: "x \<le> SUPR A f \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)"
+lemma le_SUP_iff: "x \<le> SUPREMUM A f \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)"
   using le_Sup_iff [of _ "f ` A"] by simp
 
 subclass complete_distrib_lattice
@@ -696,11 +696,11 @@
   by auto
 
 lemma INF_bool_eq [simp]:
-  "INFI = Ball"
+  "INFIMUM = Ball"
   by (simp add: fun_eq_iff INF_def)
 
 lemma SUP_bool_eq [simp]:
-  "SUPR = Bex"
+  "SUPREMUM = Bex"
   by (simp add: fun_eq_iff SUP_def)
 
 instance bool :: complete_boolean_algebra proof
@@ -887,7 +887,7 @@
 subsubsection {* Intersections of families *}
 
 abbreviation INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
-  "INTER \<equiv> INFI"
+  "INTER \<equiv> INFIMUM"
 
 text {*
   Note: must use name @{const INTER} here instead of @{text INT}
@@ -1067,7 +1067,7 @@
 subsubsection {* Unions of families *}
 
 abbreviation UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
-  "UNION \<equiv> SUPR"
+  "UNION \<equiv> SUPREMUM"
 
 text {*
   Note: must use name @{const UNION} here instead of @{text UN}
diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Conditionally_Complete_Lattices.thy
--- a/src/HOL/Conditionally_Complete_Lattices.thy	Wed Mar 19 17:06:02 2014 +0000
+++ b/src/HOL/Conditionally_Complete_Lattices.thy	Wed Mar 19 18:47:22 2014 +0100
@@ -274,22 +274,22 @@
 lemma cInf_atLeastAtMost[simp]: "y \<le> x \<Longrightarrow> Inf {y..x} = y"
   by (auto intro!: cInf_eq_minimum)
 
-lemma cINF_lower: "bdd_below (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> INFI A f \<le> f x"
+lemma cINF_lower: "bdd_below (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> INFIMUM A f \<le> f x"
   using cInf_lower [of _ "f ` A"] by simp
 
-lemma cINF_greatest: "A \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> m \<le> f x) \<Longrightarrow> m \<le> INFI A f"
+lemma cINF_greatest: "A \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> m \<le> f x) \<Longrightarrow> m \<le> INFIMUM A f"
   using cInf_greatest [of "f ` A"] by auto
 
-lemma cSUP_upper: "x \<in> A \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> f x \<le> SUPR A f"
+lemma cSUP_upper: "x \<in> A \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> f x \<le> SUPREMUM A f"
   using cSup_upper [of _ "f ` A"] by simp
 
-lemma cSUP_least: "A \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<le> M) \<Longrightarrow> SUPR A f \<le> M"
+lemma cSUP_least: "A \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<le> M) \<Longrightarrow> SUPREMUM A f \<le> M"
   using cSup_least [of "f ` A"] by auto
 
-lemma cINF_lower2: "bdd_below (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> f x \<le> u \<Longrightarrow> INFI A f \<le> u"
+lemma cINF_lower2: "bdd_below (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> f x \<le> u \<Longrightarrow> INFIMUM A f \<le> u"
   by (auto intro: cINF_lower assms order_trans)
 
-lemma cSUP_upper2: "bdd_above (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> u \<le> f x \<Longrightarrow> u \<le> SUPR A f"
+lemma cSUP_upper2: "bdd_above (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> u \<le> f x \<Longrightarrow> u \<le> SUPREMUM A f"
   by (auto intro: cSUP_upper assms order_trans)
 
 lemma cSUP_const: "A \<noteq> {} \<Longrightarrow> (SUP x:A. c) = c"
@@ -298,10 +298,10 @@
 lemma cINF_const: "A \<noteq> {} \<Longrightarrow> (INF x:A. c) = c"
   by (intro antisym cINF_greatest) (auto intro: cINF_lower)
 
-lemma le_cINF_iff: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> u \<le> INFI A f \<longleftrightarrow> (\<forall>x\<in>A. u \<le> f x)"
+lemma le_cINF_iff: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> u \<le> INFIMUM A f \<longleftrightarrow> (\<forall>x\<in>A. u \<le> f x)"
   by (metis cINF_greatest cINF_lower assms order_trans)
 
-lemma cSUP_le_iff: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> SUPR A f \<le> u \<longleftrightarrow> (\<forall>x\<in>A. f x \<le> u)"
+lemma cSUP_le_iff: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> SUPREMUM A f \<le> u \<longleftrightarrow> (\<forall>x\<in>A. f x \<le> u)"
   by (metis cSUP_least cSUP_upper assms order_trans)
 
 lemma less_cINF_D: "bdd_below (f`A) \<Longrightarrow> y < (INF i:A. f i) \<Longrightarrow> i \<in> A \<Longrightarrow> y < f i"
@@ -310,22 +310,22 @@
 lemma cSUP_lessD: "bdd_above (f`A) \<Longrightarrow> (SUP i:A. f i) < y \<Longrightarrow> i \<in> A \<Longrightarrow> f i < y"
   by (metis cSUP_upper le_less_trans)
 
-lemma cINF_insert: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> INFI (insert a A) f = inf (f a) (INFI A f)"
+lemma cINF_insert: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> INFIMUM (insert a A) f = inf (f a) (INFIMUM A f)"
   by (metis cInf_insert Inf_image_eq image_insert image_is_empty)
 
-lemma cSUP_insert: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> SUPR (insert a A) f = sup (f a) (SUPR A f)"
+lemma cSUP_insert: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> SUPREMUM (insert a A) f = sup (f a) (SUPREMUM A f)"
   by (metis cSup_insert Sup_image_eq image_insert image_is_empty)
 
-lemma cINF_mono: "B \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> (\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<le> g m) \<Longrightarrow> INFI A f \<le> INFI B g"
+lemma cINF_mono: "B \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> (\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<le> g m) \<Longrightarrow> INFIMUM A f \<le> INFIMUM B g"
   using cInf_mono [of "g ` B" "f ` A"] by auto
 
-lemma cSUP_mono: "A \<noteq> {} \<Longrightarrow> bdd_above (g ` B) \<Longrightarrow> (\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<le> g m) \<Longrightarrow> SUPR A f \<le> SUPR B g"
+lemma cSUP_mono: "A \<noteq> {} \<Longrightarrow> bdd_above (g ` B) \<Longrightarrow> (\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<le> g m) \<Longrightarrow> SUPREMUM A f \<le> SUPREMUM B g"
   using cSup_mono [of "f ` A" "g ` B"] by auto
 
-lemma cINF_superset_mono: "A \<noteq> {} \<Longrightarrow> bdd_below (g ` B) \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> g x \<le> f x) \<Longrightarrow> INFI B g \<le> INFI A f"
+lemma cINF_superset_mono: "A \<noteq> {} \<Longrightarrow> bdd_below (g ` B) \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> g x \<le> f x) \<Longrightarrow> INFIMUM B g \<le> INFIMUM A f"
   by (rule cINF_mono) auto
 
-lemma cSUP_subset_mono: "A \<noteq> {} \<Longrightarrow> bdd_above (g ` B) \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<le> g x) \<Longrightarrow> SUPR A f \<le> SUPR B g"
+lemma cSUP_subset_mono: "A \<noteq> {} \<Longrightarrow> bdd_above (g ` B) \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<le> g x) \<Longrightarrow> SUPREMUM A f \<le> SUPREMUM B g"
   by (rule cSUP_mono) auto
 
 lemma less_eq_cInf_inter: "bdd_below A \<Longrightarrow> bdd_below B \<Longrightarrow> A \<inter> B \<noteq> {} \<Longrightarrow> inf (Inf A) (Inf B) \<le> Inf (A \<inter> B)"
@@ -337,20 +337,20 @@
 lemma cInf_union_distrib: "A \<noteq> {} \<Longrightarrow> bdd_below A \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_below B \<Longrightarrow> Inf (A \<union> B) = inf (Inf A) (Inf B)"
   by (intro antisym le_infI cInf_greatest cInf_lower) (auto intro: le_infI1 le_infI2 cInf_lower)
 
-lemma cINF_union: "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_below (f`B) \<Longrightarrow> INFI (A \<union> B) f = inf (INFI A f) (INFI B f)"
+lemma cINF_union: "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_below (f`B) \<Longrightarrow> INFIMUM (A \<union> B) f = inf (INFIMUM A f) (INFIMUM B f)"
   using cInf_union_distrib [of "f ` A" "f ` B"] by (simp add: image_Un [symmetric])
 
 lemma cSup_union_distrib: "A \<noteq> {} \<Longrightarrow> bdd_above A \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_above B \<Longrightarrow> Sup (A \<union> B) = sup (Sup A) (Sup B)"
   by (intro antisym le_supI cSup_least cSup_upper) (auto intro: le_supI1 le_supI2 cSup_upper)
 
-lemma cSUP_union: "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_above (f`B) \<Longrightarrow> SUPR (A \<union> B) f = sup (SUPR A f) (SUPR B f)"
+lemma cSUP_union: "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_above (f`B) \<Longrightarrow> SUPREMUM (A \<union> B) f = sup (SUPREMUM A f) (SUPREMUM B f)"
   using cSup_union_distrib [of "f ` A" "f ` B"] by (simp add: image_Un [symmetric])
 
-lemma cINF_inf_distrib: "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> bdd_below (g`A) \<Longrightarrow> inf (INFI A f) (INFI A g) = (INF a:A. inf (f a) (g a))"
+lemma cINF_inf_distrib: "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> bdd_below (g`A) \<Longrightarrow> inf (INFIMUM A f) (INFIMUM A g) = (INF a:A. inf (f a) (g a))"
   by (intro antisym le_infI cINF_greatest cINF_lower2)
      (auto intro: le_infI1 le_infI2 cINF_greatest cINF_lower le_infI)
 
-lemma SUP_sup_distrib: "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> bdd_above (g`A) \<Longrightarrow> sup (SUPR A f) (SUPR A g) = (SUP a:A. sup (f a) (g a))"
+lemma SUP_sup_distrib: "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> bdd_above (g`A) \<Longrightarrow> sup (SUPREMUM A f) (SUPREMUM A g) = (SUP a:A. sup (f a) (g a))"
   by (intro antisym le_supI cSUP_least cSUP_upper2)
      (auto intro: le_supI1 le_supI2 cSUP_least cSUP_upper le_supI)
 
diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Mar 19 17:06:02 2014 +0000
+++ b/src/HOL/Finite_Set.thy	Wed Mar 19 18:47:22 2014 +0100
@@ -1035,7 +1035,7 @@
 
 lemma inf_INF_fold_inf:
   assumes "finite A"
-  shows "inf B (INFI A f) = fold (inf \<circ> f) B A" (is "?inf = ?fold") 
+  shows "inf B (INFIMUM A f) = fold (inf \<circ> f) B A" (is "?inf = ?fold") 
 proof (rule sym)
   interpret comp_fun_idem inf by (fact comp_fun_idem_inf)
   interpret comp_fun_idem "inf \<circ> f" by (fact comp_comp_fun_idem)
@@ -1046,7 +1046,7 @@
 
 lemma sup_SUP_fold_sup:
   assumes "finite A"
-  shows "sup B (SUPR A f) = fold (sup \<circ> f) B A" (is "?sup = ?fold") 
+  shows "sup B (SUPREMUM A f) = fold (sup \<circ> f) B A" (is "?sup = ?fold") 
 proof (rule sym)
   interpret comp_fun_idem sup by (fact comp_fun_idem_sup)
   interpret comp_fun_idem "sup \<circ> f" by (fact comp_comp_fun_idem)
@@ -1057,12 +1057,12 @@
 
 lemma INF_fold_inf:
   assumes "finite A"
-  shows "INFI A f = fold (inf \<circ> f) top A"
+  shows "INFIMUM A f = fold (inf \<circ> f) top A"
   using assms inf_INF_fold_inf [of A top] by simp
 
 lemma SUP_fold_sup:
   assumes "finite A"
-  shows "SUPR A f = fold (sup \<circ> f) bot A"
+  shows "SUPREMUM A f = fold (sup \<circ> f) bot A"
   using assms sup_SUP_fold_sup [of A bot] by simp
 
 end
diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Wed Mar 19 17:06:02 2014 +0000
+++ b/src/HOL/GCD.thy	Wed Mar 19 18:47:22 2014 +0100
@@ -1558,8 +1558,8 @@
 interpretation gcd_lcm_complete_lattice_nat:
   complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat"
 where
-  "Inf.INFI Gcd A f = Gcd (f ` A :: nat set)"
-  and "Sup.SUPR Lcm A f = Lcm (f ` A)"
+  "Inf.INFIMUM Gcd A f = Gcd (f ` A :: nat set)"
+  and "Sup.SUPREMUM Lcm A f = Lcm (f ` A)"
 proof -
   show "class.complete_lattice Gcd Lcm gcd Rings.dvd (\<lambda>m n. m dvd n \<and> \<not> n dvd m) lcm 1 (0::nat)"
   proof
@@ -1577,8 +1577,8 @@
   qed
   then interpret gcd_lcm_complete_lattice_nat:
     complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat" .
-  from gcd_lcm_complete_lattice_nat.INF_def show "Inf.INFI Gcd A f = Gcd (f ` A)" .
-  from gcd_lcm_complete_lattice_nat.SUP_def show "Sup.SUPR Lcm A f = Lcm (f ` A)" .
+  from gcd_lcm_complete_lattice_nat.INF_def show "Inf.INFIMUM Gcd A f = Gcd (f ` A)" .
+  from gcd_lcm_complete_lattice_nat.SUP_def show "Sup.SUPREMUM Lcm A f = Lcm (f ` A)" .
 qed
 
 declare gcd_lcm_complete_lattice_nat.Inf_image_eq [simp del]
diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Wed Mar 19 17:06:02 2014 +0000
+++ b/src/HOL/Library/Extended_Real.thy	Wed Mar 19 18:47:22 2014 +0100
@@ -1411,15 +1411,15 @@
 
 lemma ereal_SUP_not_infty:
   fixes f :: "_ \<Rightarrow> ereal"
-  shows "A \<noteq> {} \<Longrightarrow> l \<noteq> -\<infinity> \<Longrightarrow> u \<noteq> \<infinity> \<Longrightarrow> \<forall>a\<in>A. l \<le> f a \<and> f a \<le> u \<Longrightarrow> \<bar>SUPR A f\<bar> \<noteq> \<infinity>"
+  shows "A \<noteq> {} \<Longrightarrow> l \<noteq> -\<infinity> \<Longrightarrow> u \<noteq> \<infinity> \<Longrightarrow> \<forall>a\<in>A. l \<le> f a \<and> f a \<le> u \<Longrightarrow> \<bar>SUPREMUM A f\<bar> \<noteq> \<infinity>"
   using SUP_upper2[of _ A l f] SUP_least[of A f u]
-  by (cases "SUPR A f") auto
+  by (cases "SUPREMUM A f") auto
 
 lemma ereal_INF_not_infty:
   fixes f :: "_ \<Rightarrow> ereal"
-  shows "A \<noteq> {} \<Longrightarrow> l \<noteq> -\<infinity> \<Longrightarrow> u \<noteq> \<infinity> \<Longrightarrow> \<forall>a\<in>A. l \<le> f a \<and> f a \<le> u \<Longrightarrow> \<bar>INFI A f\<bar> \<noteq> \<infinity>"
+  shows "A \<noteq> {} \<Longrightarrow> l \<noteq> -\<infinity> \<Longrightarrow> u \<noteq> \<infinity> \<Longrightarrow> \<forall>a\<in>A. l \<le> f a \<and> f a \<le> u \<Longrightarrow> \<bar>INFIMUM A f\<bar> \<noteq> \<infinity>"
   using INF_lower2[of _ A f u] INF_greatest[of A l f]
-  by (cases "INFI A f") auto
+  by (cases "INFIMUM A f") auto
 
 lemma ereal_SUP_uminus:
   fixes f :: "'a \<Rightarrow> ereal"
@@ -1528,12 +1528,12 @@
   fixes f :: "'i \<Rightarrow> ereal"
   assumes "\<And>i. f i + y \<le> z"
     and "y \<noteq> -\<infinity>"
-  shows "SUPR UNIV f + y \<le> z"
+  shows "SUPREMUM UNIV f + y \<le> z"
 proof (cases y)
   case (real r)
   then have "\<And>i. f i \<le> z - y"
     using assms by (simp add: ereal_le_minus_iff)
-  then have "SUPR UNIV f \<le> z - y"
+  then have "SUPREMUM UNIV f \<le> z - y"
     by (rule SUP_least)
   then show ?thesis
     using real by (simp add: ereal_le_minus_iff)
@@ -1544,11 +1544,11 @@
   assumes "incseq f"
     and "incseq g"
     and pos: "\<And>i. f i \<noteq> -\<infinity>" "\<And>i. g i \<noteq> -\<infinity>"
-  shows "(SUP i. f i + g i) = SUPR UNIV f + SUPR UNIV g"
+  shows "(SUP i. f i + g i) = SUPREMUM UNIV f + SUPREMUM UNIV g"
 proof (rule SUP_eqI)
   fix y
   assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> f i + g i \<le> y"
-  have f: "SUPR UNIV f \<noteq> -\<infinity>"
+  have f: "SUPREMUM UNIV f \<noteq> -\<infinity>"
     using pos
     unfolding SUP_def Sup_eq_MInfty
     by (auto dest: image_eqD)
@@ -1565,13 +1565,13 @@
       also have "\<dots> \<le> y" using * by auto
       finally have "f i + g j \<le> y" .
     }
-    then have "SUPR UNIV f + g j \<le> y"
+    then have "SUPREMUM UNIV f + g j \<le> y"
       using assms(4)[of j] by (intro SUP_ereal_le_addI) auto
-    then have "g j + SUPR UNIV f \<le> y" by (simp add: ac_simps)
+    then have "g j + SUPREMUM UNIV f \<le> y" by (simp add: ac_simps)
   }
-  then have "SUPR UNIV g + SUPR UNIV f \<le> y"
+  then have "SUPREMUM UNIV g + SUPREMUM UNIV f \<le> y"
     using f by (rule SUP_ereal_le_addI)
-  then show "SUPR UNIV f + SUPR UNIV g \<le> y"
+  then show "SUPREMUM UNIV f + SUPREMUM UNIV g \<le> y"
     by (simp add: ac_simps)
 qed (auto intro!: add_mono SUP_upper)
 
@@ -1579,7 +1579,7 @@
   fixes f g :: "nat \<Rightarrow> ereal"
   assumes inc: "incseq f" "incseq g"
     and pos: "\<And>i. 0 \<le> f i" "\<And>i. 0 \<le> g i"
-  shows "(SUP i. f i + g i) = SUPR UNIV f + SUPR UNIV g"
+  shows "(SUP i. f i + g i) = SUPREMUM UNIV f + SUPREMUM UNIV g"
 proof (intro SUP_ereal_add inc)
   fix i
   show "f i \<noteq> -\<infinity>" "g i \<noteq> -\<infinity>"
@@ -1590,7 +1590,7 @@
   fixes f g :: "'a \<Rightarrow> nat \<Rightarrow> ereal"
   assumes "\<And>n. n \<in> A \<Longrightarrow> incseq (f n)"
     and pos: "\<And>n i. n \<in> A \<Longrightarrow> 0 \<le> f n i"
-  shows "(SUP i. \<Sum>n\<in>A. f n i) = (\<Sum>n\<in>A. SUPR UNIV (f n))"
+  shows "(SUP i. \<Sum>n\<in>A. f n i) = (\<Sum>n\<in>A. SUPREMUM UNIV (f n))"
 proof (cases "finite A")
   case True
   then show ?thesis using assms
@@ -1604,20 +1604,20 @@
   fixes f :: "nat \<Rightarrow> ereal"
   assumes "\<And>i. 0 \<le> f i"
     and "0 \<le> c"
-  shows "(SUP i. c * f i) = c * SUPR UNIV f"
+  shows "(SUP i. c * f i) = c * SUPREMUM UNIV f"
 proof (rule SUP_eqI)
   fix i
-  have "f i \<le> SUPR UNIV f"
+  have "f i \<le> SUPREMUM UNIV f"
     by (rule SUP_upper) auto
-  then show "c * f i \<le> c * SUPR UNIV f"
+  then show "c * f i \<le> c * SUPREMUM UNIV f"
     using `0 \<le> c` by (rule ereal_mult_left_mono)
 next
   fix y
   assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> c * f i \<le> y"
-  show "c * SUPR UNIV f \<le> y"
+  show "c * SUPREMUM UNIV f \<le> y"
   proof (cases "0 < c \<and> c \<noteq> \<infinity>")
     case True
-    with * have "SUPR UNIV f \<le> y / c"
+    with * have "SUPREMUM UNIV f \<le> y / c"
       by (intro SUP_least) (auto simp: ereal_le_divide_pos)
     with True show ?thesis
       by (auto simp: ereal_le_divide_pos)
@@ -1630,7 +1630,7 @@
         case True
         then have "range f = {0}"
           by auto
-        with True show "c * SUPR UNIV f \<le> y"
+        with True show "c * SUPREMUM UNIV f \<le> y"
           using * by (auto simp: SUP_def max.absorb1)
       next
         case False
@@ -1677,7 +1677,7 @@
 
 lemma Sup_countable_SUP:
   assumes "A \<noteq> {}"
-  shows "\<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> A \<and> Sup A = SUPR UNIV f"
+  shows "\<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> A \<and> Sup A = SUPREMUM UNIV f"
 proof (cases "Sup A")
   case (real r)
   have "\<forall>n::nat. \<exists>x. x \<in> A \<and> Sup A < x + 1 / ereal (real n)"
@@ -1691,7 +1691,7 @@
   qed
   from choice[OF this] obtain f :: "nat \<Rightarrow> ereal"
     where f: "\<forall>x. f x \<in> A \<and> Sup A < f x + 1 / ereal (real x)" ..
-  have "SUPR UNIV f = Sup A"
+  have "SUPREMUM UNIV f = Sup A"
   proof (rule SUP_eqI)
     fix i
     show "f i \<le> Sup A"
@@ -1752,7 +1752,7 @@
     qed
     from choice[OF this] obtain f :: "nat \<Rightarrow> ereal"
       where f: "\<forall>z. f z \<in> A \<and> x + ereal (real z) \<le> f z" ..
-    have "SUPR UNIV f = \<infinity>"
+    have "SUPREMUM UNIV f = \<infinity>"
     proof (rule SUP_PInfty)
       fix n :: nat
       show "\<exists>i\<in>UNIV. ereal (real n) \<le> f i"
@@ -1771,7 +1771,7 @@
 qed
 
 lemma SUP_countable_SUP:
-  "A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> g`A \<and> SUPR A g = SUPR UNIV f"
+  "A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> g`A \<and> SUPREMUM A g = SUPREMUM UNIV f"
   using Sup_countable_SUP [of "g`A"]
   by auto
 
@@ -1852,7 +1852,7 @@
   fixes f :: "nat \<Rightarrow> ereal"
   assumes "decseq f" "decseq g"
     and fin: "\<And>i. f i \<noteq> \<infinity>" "\<And>i. g i \<noteq> \<infinity>"
-  shows "(INF i. f i + g i) = INFI UNIV f + INFI UNIV g"
+  shows "(INF i. f i + g i) = INFIMUM UNIV f + INFIMUM UNIV g"
 proof -
   have INF_less: "(INF i. f i) < \<infinity>" "(INF i. g i) < \<infinity>"
     using assms unfolding INF_less_iff by auto
@@ -1863,7 +1863,7 @@
   }
   then have "(INF i. f i + g i) = (INF i. - ((- f i) + (- g i)))"
     by simp
-  also have "\<dots> = INFI UNIV f + INFI UNIV g"
+  also have "\<dots> = INFIMUM UNIV f + INFIMUM UNIV g"
     unfolding ereal_INF_uminus
     using assms INF_less
     by (subst SUP_ereal_add)
diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Library/Kleene_Algebra.thy
--- a/src/HOL/Library/Kleene_Algebra.thy	Wed Mar 19 17:06:02 2014 +0000
+++ b/src/HOL/Library/Kleene_Algebra.thy	Wed Mar 19 18:47:22 2014 +0100
@@ -367,7 +367,7 @@
 
 class kleene_by_complete_lattice = pre_kleene
   + complete_lattice + power + star +
-  assumes star_cont: "a * star b * c = SUPR UNIV (\<lambda>n. a * b ^ n * c)"
+  assumes star_cont: "a * star b * c = SUPREMUM UNIV (\<lambda>n. a * b ^ n * c)"
 begin
 
 subclass kleene
diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Library/Liminf_Limsup.thy
--- a/src/HOL/Library/Liminf_Limsup.thy	Wed Mar 19 17:06:02 2014 +0000
+++ b/src/HOL/Library/Liminf_Limsup.thy	Wed Mar 19 18:47:22 2014 +0100
@@ -43,13 +43,13 @@
 abbreviation "limsup \<equiv> Limsup sequentially"
 
 lemma Liminf_eqI:
-  "(\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> x) \<Longrightarrow>  
-    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x"
+  "(\<And>P. eventually P F \<Longrightarrow> INFIMUM (Collect P) f \<le> x) \<Longrightarrow>  
+    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> INFIMUM (Collect P) f \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x"
   unfolding Liminf_def by (auto intro!: SUP_eqI)
 
 lemma Limsup_eqI:
-  "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPR (Collect P) f) \<Longrightarrow>  
-    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x"
+  "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPREMUM (Collect P) f) \<Longrightarrow>  
+    (\<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)"
@@ -93,7 +93,7 @@
 proof (safe intro!: SUP_mono)
   fix P assume "eventually P F"
   with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
-  then show "\<exists>Q\<in>{P. eventually P F}. INFI (Collect P) f \<le> INFI (Collect Q) g"
+  then show "\<exists>Q\<in>{P. eventually P F}. INFIMUM (Collect P) f \<le> INFIMUM (Collect Q) g"
     by (intro bexI[of _ ?Q]) (auto intro!: INF_mono)
 qed
 
@@ -109,7 +109,7 @@
 proof (safe intro!: INF_mono)
   fix P assume "eventually P F"
   with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
-  then show "\<exists>Q\<in>{P. eventually P F}. SUPR (Collect Q) f \<le> SUPR (Collect P) g"
+  then show "\<exists>Q\<in>{P. eventually P F}. SUPREMUM (Collect Q) f \<le> SUPREMUM (Collect P) g"
     by (intro bexI[of _ ?Q]) (auto intro!: SUP_mono)
 qed
 
@@ -129,13 +129,13 @@
   then have "eventually (\<lambda>x. P x \<and> Q x) F" (is "eventually ?C F") by (rule eventually_conj)
   then have not_False: "(\<lambda>x. P x \<and> Q x) \<noteq> (\<lambda>x. False)"
     using ntriv by (auto simp add: eventually_False)
-  have "INFI (Collect P) f \<le> INFI (Collect ?C) f"
+  have "INFIMUM (Collect P) f \<le> INFIMUM (Collect ?C) f"
     by (rule INF_mono) auto
-  also have "\<dots> \<le> SUPR (Collect ?C) f"
+  also have "\<dots> \<le> SUPREMUM (Collect ?C) f"
     using not_False by (intro INF_le_SUP) auto
-  also have "\<dots> \<le> SUPR (Collect Q) f"
+  also have "\<dots> \<le> SUPREMUM (Collect Q) f"
     by (rule SUP_mono) auto
-  finally show "INFI (Collect P) f \<le> SUPR (Collect Q) f" .
+  finally show "INFIMUM (Collect P) f \<le> SUPREMUM (Collect Q) f" .
 qed
 
 lemma Liminf_bounded:
@@ -154,22 +154,22 @@
   fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
   shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)"
 proof -
-  { fix y P assume "eventually P F" "y < INFI (Collect P) X"
+  { fix y P assume "eventually P F" "y < INFIMUM (Collect P) X"
     then have "eventually (\<lambda>x. y < X x) F"
       by (auto elim!: eventually_elim1 dest: less_INF_D) }
   moreover
   { fix y P assume "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F"
-    have "\<exists>P. eventually P F \<and> y < INFI (Collect P) X"
+    have "\<exists>P. eventually P F \<and> y < INFIMUM (Collect P) X"
     proof (cases "\<exists>z. y < z \<and> z < C")
       case True
       then obtain z where z: "y < z \<and> z < C" ..
-      moreover from z have "z \<le> INFI {x. z < X x} X"
+      moreover from z have "z \<le> INFIMUM {x. z < X x} X"
         by (auto intro!: INF_greatest)
       ultimately show ?thesis
         using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto
     next
       case False
-      then have "C \<le> INFI {x. y < X x} X"
+      then have "C \<le> INFIMUM {x. y < X x} X"
         by (intro INF_greatest) auto
       with `y < C` show ?thesis
         using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto
@@ -185,17 +185,17 @@
   shows "Liminf F f = f0"
 proof (intro Liminf_eqI)
   fix P assume P: "eventually P F"
-  then have "eventually (\<lambda>x. INFI (Collect P) f \<le> f x) F"
+  then have "eventually (\<lambda>x. INFIMUM (Collect P) f \<le> f x) F"
     by eventually_elim (auto intro!: INF_lower)
-  then show "INFI (Collect P) f \<le> f0"
+  then show "INFIMUM (Collect P) f \<le> f0"
     by (rule tendsto_le[OF ntriv lim tendsto_const])
 next
-  fix y assume upper: "\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y"
+  fix y assume upper: "\<And>P. eventually P F \<Longrightarrow> INFIMUM (Collect P) f \<le> y"
   show "f0 \<le> y"
   proof cases
     assume "\<exists>z. y < z \<and> z < f0"
     then obtain z where "y < z \<and> z < f0" ..
-    moreover have "z \<le> INFI {x. z < f x} f"
+    moreover have "z \<le> INFIMUM {x. z < f x} f"
       by (rule INF_greatest) simp
     ultimately show ?thesis
       using lim[THEN topological_tendstoD, THEN upper, of "{z <..}"] by auto
@@ -208,9 +208,9 @@
         using lim[THEN topological_tendstoD, of "{y <..}"] by auto
       then have "eventually (\<lambda>x. f0 \<le> f x) F"
         using discrete by (auto elim!: eventually_elim1)
-      then have "INFI {x. f0 \<le> f x} f \<le> y"
+      then have "INFIMUM {x. f0 \<le> f x} f \<le> y"
         by (rule upper)
-      moreover have "f0 \<le> INFI {x. f0 \<le> f x} f"
+      moreover have "f0 \<le> INFIMUM {x. f0 \<le> f x} f"
         by (intro INF_greatest) simp
       ultimately show "f0 \<le> y" by simp
     qed
@@ -224,17 +224,17 @@
   shows "Limsup F f = f0"
 proof (intro Limsup_eqI)
   fix P assume P: "eventually P F"
-  then have "eventually (\<lambda>x. f x \<le> SUPR (Collect P) f) F"
+  then have "eventually (\<lambda>x. f x \<le> SUPREMUM (Collect P) f) F"
     by eventually_elim (auto intro!: SUP_upper)
-  then show "f0 \<le> SUPR (Collect P) f"
+  then show "f0 \<le> SUPREMUM (Collect P) f"
     by (rule tendsto_le[OF ntriv tendsto_const lim])
 next
-  fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f"
+  fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPREMUM (Collect P) f"
   show "y \<le> f0"
   proof (cases "\<exists>z. f0 < z \<and> z < y")
     case True
     then obtain z where "f0 < z \<and> z < y" ..
-    moreover have "SUPR {x. f x < z} f \<le> z"
+    moreover have "SUPREMUM {x. f x < z} f \<le> z"
       by (rule SUP_least) simp
     ultimately show ?thesis
       using lim[THEN topological_tendstoD, THEN lower, of "{..< z}"] by auto
@@ -247,9 +247,9 @@
         using lim[THEN topological_tendstoD, of "{..< y}"] by auto
       then have "eventually (\<lambda>x. f x \<le> f0) F"
         using False by (auto elim!: eventually_elim1 simp: not_less)
-      then have "y \<le> SUPR {x. f x \<le> f0} f"
+      then have "y \<le> SUPREMUM {x. f x \<le> f0} f"
         by (rule lower)
-      moreover have "SUPR {x. f x \<le> f0} f \<le> f0"
+      moreover have "SUPREMUM {x. f x \<le> f0} f \<le> f0"
         by (intro SUP_least) simp
       ultimately show "y \<le> f0" by simp
     qed
@@ -264,14 +264,14 @@
 proof (rule order_tendstoI)
   fix a assume "f0 < a"
   with assms have "Limsup F f < a" by simp
-  then obtain P where "eventually P F" "SUPR (Collect P) f < a"
+  then obtain P where "eventually P F" "SUPREMUM (Collect P) f < a"
     unfolding Limsup_def INF_less_iff by auto
   then show "eventually (\<lambda>x. f x < a) F"
     by (auto elim!: eventually_elim1 dest: SUP_lessD)
 next
   fix a assume "a < f0"
   with assms have "a < Liminf F f" by simp
-  then obtain P where "eventually P F" "a < INFI (Collect P) f"
+  then obtain P where "eventually P F" "a < INFIMUM (Collect P) f"
     unfolding Liminf_def less_SUP_iff by auto
   then show "eventually (\<lambda>x. a < f x) F"
     by (auto elim!: eventually_elim1 dest: less_INF_D)
diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Library/Product_Order.thy
--- a/src/HOL/Library/Product_Order.thy	Wed Mar 19 17:06:02 2014 +0000
+++ b/src/HOL/Library/Product_Order.thy	Wed Mar 19 18:47:22 2014 +0100
@@ -219,11 +219,11 @@
 of two complete lattices: *}
 
 lemma INF_prod_alt_def:
-  "INFI A f = (INFI A (fst o f), INFI A (snd o f))"
+  "INFIMUM A f = (INFIMUM A (fst o f), INFIMUM A (snd o f))"
   unfolding INF_def Inf_prod_def by simp
 
 lemma SUP_prod_alt_def:
-  "SUPR A f = (SUPR A (fst o f), SUPR A (snd o f))"
+  "SUPREMUM A f = (SUPREMUM A (fst o f), SUPREMUM A (snd o f))"
   unfolding SUP_def Sup_prod_def by simp
 
 
diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Library/RBT_Set.thy
--- a/src/HOL/Library/RBT_Set.thy	Wed Mar 19 17:06:02 2014 +0000
+++ b/src/HOL/Library/RBT_Set.thy	Wed Mar 19 18:47:22 2014 +0100
@@ -112,7 +112,7 @@
   "Inf_fin = Inf_fin" ..
 
 lemma [code, code del]:
-  "INFI = INFI" ..
+  "INFIMUM = INFIMUM" ..
 
 lemma [code, code del]:
   "Max = Max" ..
@@ -121,7 +121,7 @@
   "Sup_fin = Sup_fin" ..
 
 lemma [code, code del]:
-  "SUPR = SUPR" ..
+  "SUPREMUM = SUPREMUM" ..
 
 lemma [code, code del]:
   "(Inf :: 'a set set \<Rightarrow> 'a set) = Inf" ..
@@ -759,7 +759,7 @@
 
 lemma INF_Set_fold [code]:
   fixes f :: "_ \<Rightarrow> 'a::complete_lattice"
-  shows "INFI (Set t) f = fold_keys (inf \<circ> f) t top"
+  shows "INFIMUM (Set t) f = fold_keys (inf \<circ> f) t top"
 proof -
   have "comp_fun_commute ((inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
     by default (auto simp add: fun_eq_iff ac_simps)
@@ -800,7 +800,7 @@
 
 lemma SUP_Set_fold [code]:
   fixes f :: "_ \<Rightarrow> 'a::complete_lattice"
-  shows "SUPR (Set t) f = fold_keys (sup \<circ> f) t bot"
+  shows "SUPREMUM (Set t) f = fold_keys (sup \<circ> f) t bot"
 proof -
   have "comp_fun_commute ((sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
     by default (auto simp add: fun_eq_iff ac_simps)
diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Lifting_Set.thy
--- a/src/HOL/Lifting_Set.thy	Wed Mar 19 17:06:02 2014 +0000
+++ b/src/HOL/Lifting_Set.thy	Wed Mar 19 18:47:22 2014 +0100
@@ -150,12 +150,12 @@
   unfolding rel_fun_def rel_set_def by fast
 
 lemma SUP_parametric [transfer_rule]:
-  "(rel_set R ===> (R ===> op =) ===> op =) SUPR (SUPR :: _ \<Rightarrow> _ \<Rightarrow> _::complete_lattice)"
+  "(rel_set R ===> (R ===> op =) ===> op =) SUPREMUM (SUPREMUM :: _ \<Rightarrow> _ \<Rightarrow> _::complete_lattice)"
 proof(rule rel_funI)+
   fix A B f and g :: "'b \<Rightarrow> 'c"
   assume AB: "rel_set R A B"
     and fg: "(R ===> op =) f g"
-  show "SUPR A f = SUPR B g"
+  show "SUPREMUM A f = SUPREMUM B g"
     by (rule SUP_eq) (auto 4 4 dest: rel_setD1 [OF AB] rel_setD2 [OF AB] rel_funD [OF fg] intro: rev_bexI)
 qed
 
diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Mar 19 17:06:02 2014 +0000
+++ b/src/HOL/List.thy	Wed Mar 19 18:47:22 2014 +0100
@@ -2876,13 +2876,13 @@
 declare Sup_set_fold [where 'a = "'a set", code]
 
 lemma (in complete_lattice) INF_set_fold:
-  "INFI (set xs) f = fold (inf \<circ> f) xs top"
+  "INFIMUM (set xs) f = fold (inf \<circ> f) xs top"
   using Inf_set_fold [of "map f xs "] by (simp add: fold_map)
 
 declare INF_set_fold [code]
 
 lemma (in complete_lattice) SUP_set_fold:
-  "SUPR (set xs) f = fold (sup \<circ> f) xs bot"
+  "SUPREMUM (set xs) f = fold (sup \<circ> f) xs bot"
   using Sup_set_fold [of "map f xs "] by (simp add: fold_map)
 
 declare SUP_set_fold [code]
diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Wed Mar 19 17:06:02 2014 +0000
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Wed Mar 19 18:47:22 2014 +0100
@@ -1166,13 +1166,13 @@
   assume "0 < d" and "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y"
   then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
     by (auto simp: zero_less_dist_iff dist_commute)
-  then show "\<exists>r>0. INFI (Collect P) f \<le> INFI (S \<inter> ball x r - {x}) f"
+  then show "\<exists>r>0. INFIMUM (Collect P) f \<le> INFIMUM (S \<inter> ball x r - {x}) f"
     by (intro exI[of _ d] INF_mono conjI `0 < d`) auto
 next
   fix d :: real
   assume "0 < d"
   then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> xa \<noteq> x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
-    INFI (S \<inter> ball x d - {x}) f \<le> INFI (Collect P) f"
+    INFIMUM (S \<inter> ball x d - {x}) f \<le> INFIMUM (Collect P) f"
     by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
        (auto intro!: INF_mono exI[of _ d] simp: dist_commute)
 qed
@@ -1186,13 +1186,13 @@
   assume "0 < d" and "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y"
   then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
     by (auto simp: zero_less_dist_iff dist_commute)
-  then show "\<exists>r>0. SUPR (S \<inter> ball x r - {x}) f \<le> SUPR (Collect P) f"
+  then show "\<exists>r>0. SUPREMUM (S \<inter> ball x r - {x}) f \<le> SUPREMUM (Collect P) f"
     by (intro exI[of _ d] SUP_mono conjI `0 < d`) auto
 next
   fix d :: real
   assume "0 < d"
   then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> xa \<noteq> x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
-    SUPR (Collect P) f \<le> SUPR (S \<inter> ball x d - {x}) f"
+    SUPREMUM (Collect P) f \<le> SUPREMUM (S \<inter> ball x d - {x}) f"
     by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
        (auto intro!: SUP_mono exI[of _ d] simp: dist_commute)
 qed
@@ -1285,11 +1285,11 @@
   fix P
   assume P: "eventually P net"
   fix S
-  assume S: "mono_set S" "INFI (Collect P) f \<in> S"
+  assume S: "mono_set S" "INFIMUM (Collect P) f \<in> S"
   {
     fix x
     assume "P x"
-    then have "INFI (Collect P) f \<le> f x"
+    then have "INFIMUM (Collect P) f \<le> f x"
       by (intro complete_lattice_class.INF_lower) simp
     with S have "f x \<in> S"
       by (simp add: mono_set)
@@ -1299,16 +1299,16 @@
 next
   fix y l
   assume S: "\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net"
-  assume P: "\<forall>P. eventually P net \<longrightarrow> INFI (Collect P) f \<le> y"
+  assume P: "\<forall>P. eventually P net \<longrightarrow> INFIMUM (Collect P) f \<le> y"
   show "l \<le> y"
   proof (rule dense_le)
     fix B
     assume "B < l"
     then have "eventually (\<lambda>x. f x \<in> {B <..}) net"
       by (intro S[rule_format]) auto
-    then have "INFI {x. B < f x} f \<le> y"
+    then have "INFIMUM {x. B < f x} f \<le> y"
       using P by auto
-    moreover have "B \<le> INFI {x. B < f x} f"
+    moreover have "B \<le> INFIMUM {x. B < f x} f"
       by (intro INF_greatest) auto
     ultimately show "B \<le> y"
       by simp
@@ -1324,13 +1324,13 @@
   fix P
   assume P: "eventually P net"
   fix S
-  assume S: "mono_set (uminus`S)" "SUPR (Collect P) f \<in> S"
+  assume S: "mono_set (uminus`S)" "SUPREMUM (Collect P) f \<in> S"
   {
     fix x
     assume "P x"
-    then have "f x \<le> SUPR (Collect P) f"
+    then have "f x \<le> SUPREMUM (Collect P) f"
       by (intro complete_lattice_class.SUP_upper) simp
-    with S(1)[unfolded mono_set, rule_format, of "- SUPR (Collect P) f" "- f x"] S(2)
+    with S(1)[unfolded mono_set, rule_format, of "- SUPREMUM (Collect P) f" "- f x"] S(2)
     have "f x \<in> S"
       by (simp add: inj_image_mem_iff) }
   with P show "eventually (\<lambda>x. f x \<in> S) net"
@@ -1338,16 +1338,16 @@
 next
   fix y l
   assume S: "\<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net"
-  assume P: "\<forall>P. eventually P net \<longrightarrow> y \<le> SUPR (Collect P) f"
+  assume P: "\<forall>P. eventually P net \<longrightarrow> y \<le> SUPREMUM (Collect P) f"
   show "y \<le> l"
   proof (rule dense_ge)
     fix B
     assume "l < B"
     then have "eventually (\<lambda>x. f x \<in> {..< B}) net"
       by (intro S[rule_format]) auto
-    then have "y \<le> SUPR {x. f x < B} f"
+    then have "y \<le> SUPREMUM {x. f x < B} f"
       using P by auto
-    moreover have "SUPR {x. f x < B} f \<le> B"
+    moreover have "SUPREMUM {x. f x < B} f \<le> B"
       by (intro SUP_least) auto
     ultimately show "y \<le> B"
       by simp
diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Wed Mar 19 17:06:02 2014 +0000
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Wed Mar 19 18:47:22 2014 +0100
@@ -11842,7 +11842,7 @@
         using goal2 by auto
     qed
     then obtain K where *: "\<exists>x\<in>{d. d division_of \<Union>d}. K = (\<Sum>k\<in>x. norm (integral k f))"
-      "SUPR {d. d division_of \<Union>d} (setsum (\<lambda>k. norm (integral k f))) - e < K"
+      "SUPREMUM {d. d division_of \<Union>d} (setsum (\<lambda>k. norm (integral k f))) - e < K"
       by (auto simp add: image_iff not_le)
     from this(1) obtain d where "d division_of \<Union>d"
       and "K = (\<Sum>k\<in>d. norm (integral k f))"
diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Wed Mar 19 17:06:02 2014 +0000
+++ b/src/HOL/Predicate.thy	Wed Mar 19 18:47:22 2014 +0100
@@ -65,17 +65,17 @@
   by (simp add: sup_pred_def)
 
 definition
-  "\<Sqinter>A = Pred (INFI A eval)"
+  "\<Sqinter>A = Pred (INFIMUM A eval)"
 
 lemma eval_Inf [simp]:
-  "eval (\<Sqinter>A) = INFI A eval"
+  "eval (\<Sqinter>A) = INFIMUM A eval"
   by (simp add: Inf_pred_def)
 
 definition
-  "\<Squnion>A = Pred (SUPR A eval)"
+  "\<Squnion>A = Pred (SUPREMUM A eval)"
 
 lemma eval_Sup [simp]:
-  "eval (\<Squnion>A) = SUPR A eval"
+  "eval (\<Squnion>A) = SUPREMUM A eval"
   by (simp add: Sup_pred_def)
 
 instance proof
@@ -84,11 +84,11 @@
 end
 
 lemma eval_INF [simp]:
-  "eval (INFI A f) = INFI A (eval \<circ> f)"
+  "eval (INFIMUM A f) = INFIMUM A (eval \<circ> f)"
   using eval_Inf [of "f ` A"] by simp
 
 lemma eval_SUP [simp]:
-  "eval (SUPR A f) = SUPR A (eval \<circ> f)"
+  "eval (SUPREMUM A f) = SUPREMUM A (eval \<circ> f)"
   using eval_Sup [of "f ` A"] by simp
 
 instantiation pred :: (type) complete_boolean_algebra
@@ -121,10 +121,10 @@
   by (simp add: single_def)
 
 definition bind :: "'a pred \<Rightarrow> ('a \<Rightarrow> 'b pred) \<Rightarrow> 'b pred" (infixl "\<guillemotright>=" 70) where
-  "P \<guillemotright>= f = (SUPR {x. eval P x} f)"
+  "P \<guillemotright>= f = (SUPREMUM {x. eval P x} f)"
 
 lemma eval_bind [simp]:
-  "eval (P \<guillemotright>= f) = eval (SUPR {x. eval P x} f)"
+  "eval (P \<guillemotright>= f) = eval (SUPREMUM {x. eval P x} f)"
   by (simp add: bind_def)
 
 lemma bind_bind:
diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Wed Mar 19 17:06:02 2014 +0000
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Wed Mar 19 18:47:22 2014 +0100
@@ -781,7 +781,7 @@
 
 lemma positive_integral_def_finite:
   "integral\<^sup>P M f = (SUP g : {g. simple_function M g \<and> g \<le> max 0 \<circ> f \<and> range g \<subseteq> {0 ..< \<infinity>}}. integral\<^sup>S M g)"
-    (is "_ = SUPR ?A ?f")
+    (is "_ = SUPREMUM ?A ?f")
   unfolding positive_integral_def
 proof (safe intro!: antisym SUP_least)
   fix g assume g: "simple_function M g" "g \<le> max 0 \<circ> f"
@@ -793,7 +793,7 @@
     apply (safe intro!: simple_function_max simple_function_If)
     apply (force simp: max_def le_fun_def split: split_if_asm)+
     done
-  show "integral\<^sup>S M g \<le> SUPR ?A ?f"
+  show "integral\<^sup>S M g \<le> SUPREMUM ?A ?f"
   proof cases
     have g0: "?g 0 \<in> ?A" by (intro g_in_A) auto
     assume "(emeasure M) ?G = 0"
@@ -804,7 +804,7 @@
          (auto simp: max_def intro!: simple_function_If)
   next
     assume \<mu>_G: "(emeasure M) ?G \<noteq> 0"
-    have "SUPR ?A (integral\<^sup>S M) = \<infinity>"
+    have "SUPREMUM ?A (integral\<^sup>S M) = \<infinity>"
     proof (intro SUP_PInfty)
       fix n :: nat
       let ?y = "ereal (real n) / (if (emeasure M) ?G = \<infinity> then 1 else (emeasure M) ?G)"
@@ -1029,7 +1029,7 @@
         using N(1) by auto }
   qed
   also have "\<dots> = (SUP i. (\<integral>\<^sup>+ x. f i x \<partial>M))"
-    using f_eq by (force intro!: arg_cong[where f="SUPR UNIV"] positive_integral_cong_AE ext)
+    using f_eq by (force intro!: arg_cong[where f="SUPREMUM UNIV"] positive_integral_cong_AE ext)
   finally show ?thesis .
 qed
 
@@ -1045,7 +1045,7 @@
   shows "(SUP i. integral\<^sup>S M (f i)) = (\<integral>\<^sup>+x. (SUP i. f i x) \<partial>M)"
   using assms unfolding positive_integral_monotone_convergence_SUP[OF f(1)
     f(3)[THEN borel_measurable_simple_function] f(2)]
-  by (auto intro!: positive_integral_eq_simple_integral[symmetric] arg_cong[where f="SUPR UNIV"] ext)
+  by (auto intro!: positive_integral_eq_simple_integral[symmetric] arg_cong[where f="SUPREMUM UNIV"] ext)
 
 lemma positive_integral_max_0:
   "(\<integral>\<^sup>+x. max 0 (f x) \<partial>M) = integral\<^sup>P M f"
@@ -1069,7 +1069,7 @@
   and g: "incseq g" "\<And>i x. 0 \<le> g i x" "\<And>i. simple_function M (g i)"
   and eq: "AE x in M. (SUP i. f i x) = (SUP i. g i x)"
   shows "(SUP i. integral\<^sup>S M (f i)) = (SUP i. integral\<^sup>S M (g i))"
-    (is "SUPR _ ?F = SUPR _ ?G")
+    (is "SUPREMUM _ ?F = SUPREMUM _ ?G")
 proof -
   have "(SUP i. integral\<^sup>S M (f i)) = (\<integral>\<^sup>+x. (SUP i. f i x) \<partial>M)"
     using f by (rule positive_integral_monotone_convergence_simple)
@@ -1128,7 +1128,7 @@
       by (intro AE_I2) (auto split: split_max simp add: ereal_add_nonneg_nonneg)
   qed
   also have "\<dots> = (SUP i. a * integral\<^sup>S M (u i) + integral\<^sup>S M (v i))"
-    using u(2, 6) v(2, 6) `0 \<le> a` by (auto intro!: arg_cong[where f="SUPR UNIV"] ext)
+    using u(2, 6) v(2, 6) `0 \<le> a` by (auto intro!: arg_cong[where f="SUPREMUM UNIV"] ext)
   finally have "(\<integral>\<^sup>+ x. max 0 (a * f x + g x) \<partial>M) = a * (\<integral>\<^sup>+x. max 0 (f x) \<partial>M) + (\<integral>\<^sup>+x. max 0 (g x) \<partial>M)"
     unfolding l(5)[symmetric] u(5)[symmetric] v(5)[symmetric]
     unfolding l(1)[symmetric] u(1)[symmetric] v(1)[symmetric]
diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Wed Mar 19 17:06:02 2014 +0000
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Wed Mar 19 18:47:22 2014 +0100
@@ -169,7 +169,7 @@
         by (auto intro!: SUP_upper2 integral_nonneg)
     next
       show "(SUP n. \<Sum>i. ereal (?m n i)) = (SUP n. ereal (?M n UNIV))"
-      proof (intro arg_cong[where f="SUPR UNIV"] ext sums_unique[symmetric] sums_ereal[THEN iffD2] sums_def[THEN iffD2])
+      proof (intro arg_cong[where f="SUPREMUM UNIV"] ext sums_unique[symmetric] sums_ereal[THEN iffD2] sums_def[THEN iffD2])
         fix n
         have "\<And>m. (UNION {..<m} A) \<in> sets lebesgue" using rA by auto
         from lebesgueD[OF this]
diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Mar 19 17:06:02 2014 +0000
+++ b/src/HOL/Product_Type.thy	Wed Mar 19 18:47:22 2014 +0100
@@ -342,8 +342,8 @@
   in
     [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},
      Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"},
-     Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"},
-     Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}]
+     Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFIMUM} @{syntax_const "_INF"},
+     Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPREMUM} @{syntax_const "_SUP"}]
     |> map (fn (Q, tr) => (Q, contract Q tr))
   end
 *}
diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Wed Mar 19 17:06:02 2014 +0000
+++ b/src/HOL/Relation.thy	Wed Mar 19 18:47:22 2014 +0100
@@ -281,7 +281,7 @@
   by (fast intro: symI elim: symE)
 
 lemma symp_INF:
-  "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (INFI S r)"
+  "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (INFIMUM S r)"
   by (fact sym_INTER [to_pred])
 
 lemma sym_UNION:
@@ -289,7 +289,7 @@
   by (fast intro: symI elim: symE)
 
 lemma symp_SUP:
-  "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (SUPR S r)"
+  "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (SUPREMUM S r)"
   by (fact sym_UNION [to_pred])
 
 
diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Tools/BNF/bnf_util.ML
--- a/src/HOL/Tools/BNF/bnf_util.ML	Wed Mar 19 17:06:02 2014 +0000
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Wed Mar 19 18:47:22 2014 +0100
@@ -393,7 +393,7 @@
 
 fun mk_UNION X f =
   let val (T, U) = dest_funT (fastype_of f);
-  in Const (@{const_name SUPR}, fastype_of X --> (T --> U) --> U) $ X $ f end;
+  in Const (@{const_name SUPREMUM}, fastype_of X --> (T --> U) --> U) $ X $ f end;
 
 fun mk_Union T =
   Const (@{const_name Sup}, HOLogic.mk_setT (HOLogic.mk_setT T) --> HOLogic.mk_setT T);
diff -r dc429a5b13c4 -r 1c3f1f2431f9 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Wed Mar 19 17:06:02 2014 +0000
+++ b/src/HOL/Wellfounded.thy	Wed Mar 19 18:47:22 2014 +0100
@@ -297,7 +297,7 @@
 done
 
 lemma wfP_SUP:
-  "\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (DomainP (r i)) (RangeP (r j)) = bot \<Longrightarrow> wfP (SUPR UNIV r)"
+  "\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (DomainP (r i)) (RangeP (r j)) = bot \<Longrightarrow> wfP (SUPREMUM UNIV r)"
   apply (rule wf_UN[to_pred])
   apply simp_all
   done