--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Tue Sep 03 01:12:40 2013 +0200
@@ -63,10 +63,10 @@
assumes "closed S" "S \<noteq> {}" shows "Sup S \<in> S"
proof -
from compact_eq_closed[of S] compact_attains_sup[of S] assms
- obtain s where "s \<in> S" "\<forall>t\<in>S. t \<le> s" by auto
- moreover then have "Sup S = s"
+ obtain s where S: "s \<in> S" "\<forall>t\<in>S. t \<le> s" by auto
+ then have "Sup S = s"
by (auto intro!: Sup_eqI)
- ultimately show ?thesis
+ with S show ?thesis
by simp
qed
@@ -75,10 +75,10 @@
assumes "closed S" "S \<noteq> {}" shows "Inf S \<in> S"
proof -
from compact_eq_closed[of S] compact_attains_inf[of S] assms
- obtain s where "s \<in> S" "\<forall>t\<in>S. s \<le> t" by auto
- moreover then have "Inf S = s"
+ obtain s where S: "s \<in> S" "\<forall>t\<in>S. s \<le> t" by auto
+ then have "Inf S = s"
by (auto intro!: Inf_eqI)
- ultimately show ?thesis
+ with S show ?thesis
by simp
qed