--- a/src/HOL/Real.thy Tue Mar 15 08:34:04 2016 +0100
+++ b/src/HOL/Real.thy Tue Mar 15 14:08:25 2016 +0000
@@ -1135,8 +1135,9 @@
subsection \<open>The Archimedean Property of the Reals\<close>
-lemmas reals_Archimedean = ex_inverse_of_nat_Suc_less (*FIXME*)
-lemmas reals_Archimedean2 = ex_less_of_nat
+lemma real_arch_inverse: "0 < e \<longleftrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
+ using reals_Archimedean[of e] less_trans[of 0 "1 / real n" e for n::nat]
+ by (auto simp add: field_simps cong: conj_cong simp del: of_nat_Suc)
lemma reals_Archimedean3:
assumes x_greater_zero: "0 < x"