diff -r 8bf41f8cf71d -r 7ef6505bde7f src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Wed Sep 14 10:55:07 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Wed Sep 14 10:08:52 2011 -0400
@@ -653,7 +653,7 @@
       unfolding less_SUP_iff by auto
     { fix y assume "y:S & 0 < dist y x & dist y x < d"
       hence "y:(S Int ball x d - {x})" unfolding ball_def by (auto simp add: dist_commute)
-      hence "f y:T" using d_def INF_leI[of y "S Int ball x d - {x}" f] `T={B<..}` by auto
+      hence "f y:T" using d_def INF_lower[of y "S Int ball x d - {x}" f] `T={B<..}` by auto
     } hence ?thesis apply(rule_tac x="d" in exI) using d_def by auto
   } ultimately show ?thesis by auto
   qed
@@ -669,8 +669,8 @@
       hence "y:S & 0 < dist y x & dist y x < d" unfolding ball_def apply (simp add: dist_commute)
          by (metis dist_eq_0_iff real_less_def zero_le_dist)
       hence "B <= f y" using d_def by auto
-    } hence "B <= INFI (S Int ball x d - {x}) f" apply (subst le_INFI) by auto
-    also have "...<=?l" apply (subst le_SUPI) using d_def by auto
+    } hence "B <= INFI (S Int ball x d - {x}) f" apply (subst INF_greatest) by auto
+    also have "...<=?l" apply (subst SUP_upper) using d_def by auto
     finally have "B<=?l" by auto
   } hence "z <= ?l" using ereal_le_ereal[of z "?l"] by auto
 }
@@ -700,7 +700,7 @@
       unfolding INF_less_iff by auto
     { fix y assume "y:S & 0 < dist y x & dist y x < d"
       hence "y:(S Int ball x d - {x})" unfolding ball_def by (auto simp add: dist_commute)
-      hence "f y:T" using d_def le_SUPI[of y "S Int ball x d - {x}" f] `T={..<B}` by auto
+      hence "f y:T" using d_def SUP_upper[of y "S Int ball x d - {x}" f] `T={..<B}` by auto
     } hence ?thesis apply(rule_tac x="d" in exI) using d_def by auto
   } ultimately show ?thesis by auto
   qed
@@ -716,8 +716,8 @@
       hence "y:S & 0 < dist y x & dist y x < d" unfolding ball_def apply (simp add: dist_commute)
          by (metis dist_eq_0_iff real_less_def zero_le_dist)
       hence "f y <= B" using d_def by auto
-    } hence "SUPR (S Int ball x d - {x}) f <= B" apply (subst SUP_leI) by auto
-    moreover have "?l<=SUPR (S Int ball x d - {x}) f" apply (subst INF_leI) using d_def by auto
+    } hence "SUPR (S Int ball x d - {x}) f <= B" apply (subst SUP_least) by auto
+    moreover have "?l<=SUPR (S Int ball x d - {x}) f" apply (subst INF_lower) using d_def by auto
     ultimately have "?l<=B" by auto
   } hence "?l <= z" using ereal_ge_ereal[of z "?l"] by auto
 }
@@ -1149,7 +1149,7 @@
 lemma suminf_upper:
   fixes f :: "nat \<Rightarrow> ereal" assumes "\<And>n. 0 \<le> f n"
   shows "(\<Sum>n<N. f n) \<le> (\<Sum>n. f n)"
-  unfolding suminf_ereal_eq_SUPR[OF assms] SUPR_def
+  unfolding suminf_ereal_eq_SUPR[OF assms] SUP_def
   by (auto intro: complete_lattice_class.Sup_upper image_eqI)
 
 lemma suminf_0_le:
@@ -1291,7 +1291,7 @@
   show ?thesis using assms
     apply (subst (1 2) suminf_ereal_eq_SUPR)
     unfolding *
-    apply (auto intro!: le_SUPI2)
+    apply (auto intro!: SUP_upper2)
     apply (subst SUP_commute) ..
 qed