--- a/src/HOL/Import/HOLLightReal.thy Wed Aug 31 13:28:29 2011 -0700
+++ b/src/HOL/Import/HOLLightReal.thy Thu Sep 01 16:16:25 2011 +0900
@@ -301,10 +301,7 @@
"(\<exists>(x :: real). P x) \<and> (\<exists>(M :: real). \<forall>x. P x \<longrightarrow> x \<le> M) \<longrightarrow>
(\<exists>M. (\<forall>x. P x \<longrightarrow> x \<le> M) \<and>
(\<forall>M'. (\<forall>x. P x \<longrightarrow> x \<le> M') \<longrightarrow> M \<le> M'))"
- apply (intro allI impI, elim conjE)
- apply (drule complete_real[unfolded Ball_def mem_def])
- apply simp_all
- done
+ using complete_real[unfolded Ball_def, of "Collect P"] by auto
lemma REAL_COMPLETE_SOMEPOS:
"(\<exists>(x :: real). P x \<and> 0 \<le> x) \<and> (\<exists>M. \<forall>x. P x \<longrightarrow> x \<le> M) \<longrightarrow>