# HG changeset patch
# User huffman
# Date 1179543144 -7200
# Node ID 496b42cf588d158c0aa4fb142e1466a6c6d9bd60
# Parent  3eae3140b4b267988cecd5870bb05c32f1e1c45b
remove dependence on Hilbert_Choice.thy

diff -r 3eae3140b4b2 -r 496b42cf588d src/HOL/Hyperreal/Lim.thy
--- a/src/HOL/Hyperreal/Lim.thy	Sat May 19 04:51:03 2007 +0200
+++ b/src/HOL/Hyperreal/Lim.thy	Sat May 19 04:52:24 2007 +0200
@@ -499,7 +499,7 @@
 subsection {* Uniform Continuity *}
 
 lemma isUCont_isCont: "isUCont f ==> isCont f x"
-by (simp add: isUCont_def isCont_def LIM_def, meson)
+by (simp add: isUCont_def isCont_def LIM_def, force)
 
 
 subsection {* Relation of LIM and LIMSEQ *}
diff -r 3eae3140b4b2 -r 496b42cf588d src/HOL/Real/RComplete.thy
--- a/src/HOL/Real/RComplete.thy	Sat May 19 04:51:03 2007 +0200
+++ b/src/HOL/Real/RComplete.thy	Sat May 19 04:52:24 2007 +0200
@@ -401,12 +401,13 @@
 lemma reals_Archimedean6:
      "0 \<le> r ==> \<exists>(n::nat). real (n - 1) \<le> r & r < real (n)"
 apply (insert reals_Archimedean2 [of r], safe)
-apply (frule_tac P = "%k. r < real k" and k = n and m = "%x. x"
-       in ex_has_least_nat, auto)
+apply (subgoal_tac "\<exists>x::nat. r < real x \<and> (\<forall>y. r < real y \<longrightarrow> x \<le> y)", auto)
 apply (rule_tac x = x in exI)
 apply (case_tac x, simp)
 apply (rename_tac x')
 apply (drule_tac x = x' in spec, simp)
+apply (rule_tac x="LEAST n. r < real n" in exI, safe)
+apply (erule LeastI, erule Least_le)
 done
 
 lemma reals_Archimedean6a: "0 \<le> r ==> \<exists>n. real (n) \<le> r & r < real (Suc n)"