--- a/src/HOL/Hyperreal/Fact.thy Mon Oct 11 19:36:48 2004 +0200
+++ b/src/HOL/Hyperreal/Fact.thy Tue Oct 12 11:48:21 2004 +0200
@@ -7,7 +7,7 @@
header{*Factorial Function*}
theory Fact
-imports Real
+imports "../Real/Real"
begin
consts fact :: "nat => nat"
--- a/src/HOL/Hyperreal/SEQ.thy Mon Oct 11 19:36:48 2004 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy Tue Oct 12 11:48:21 2004 +0200
@@ -1097,6 +1097,7 @@
Goal "subseq f ==> \<exists>n. N1 \<le> n & N2 \<le> f(n)";
---------------------------------------------------------------***)
+
ML
{*
val Cauchy_def = thm"Cauchy_def";
@@ -1214,15 +1215,8 @@
val monoseq_realpow = thm "monoseq_realpow";
val convergent_realpow = thm "convergent_realpow";
val NSLIMSEQ_realpow_zero = thm "NSLIMSEQ_realpow_zero";
-val LIMSEQ_realpow_zero = thm "LIMSEQ_realpow_zero";
-val LIMSEQ_divide_realpow_zero = thm "LIMSEQ_divide_realpow_zero";
-val LIMSEQ_rabs_realpow_zero = thm "LIMSEQ_rabs_realpow_zero";
-val NSLIMSEQ_rabs_realpow_zero = thm "NSLIMSEQ_rabs_realpow_zero";
-val LIMSEQ_rabs_realpow_zero2 = thm "LIMSEQ_rabs_realpow_zero2";
-val NSLIMSEQ_rabs_realpow_zero2 = thm "NSLIMSEQ_rabs_realpow_zero2";
-val NSBseq_HFinite_hypreal = thm "NSBseq_HFinite_hypreal";
-val NSLIMSEQ_zero_Infinitesimal_hypreal = thm "NSLIMSEQ_zero_Infinitesimal_hypreal";
*}
+
end
--- a/src/HOL/Hyperreal/Transcendental.thy Mon Oct 11 19:36:48 2004 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy Tue Oct 12 11:48:21 2004 +0200
@@ -2589,8 +2589,8 @@
==> \<exists>r. 0 < r & (\<forall>x. x \<noteq> c & \<bar>c - x\<bar> < r --> f x \<noteq> 0)"
apply (cut_tac x = l and y = 0 in linorder_less_linear, auto)
apply (drule LIM_fun_less_zero)
-apply (drule_tac [3] LIM_fun_gt_zero, auto)
-apply (rule_tac [!] x = r in exI, auto)
+apply (drule_tac [3] LIM_fun_gt_zero)
+apply force+
done
ML