tweaks concerned with poly bug-fixing
authorpaulson
Tue Oct 12 11:48:21 2004 +0200 (2004-10-12)
changeset 15241a3949068537e
parent 15240 e1e6db03beee
child 15242 1a4b471b1afa
tweaks concerned with poly bug-fixing
src/HOL/Hyperreal/Fact.thy
src/HOL/Hyperreal/SEQ.thy
src/HOL/Hyperreal/Transcendental.thy
     1.1 --- a/src/HOL/Hyperreal/Fact.thy	Mon Oct 11 19:36:48 2004 +0200
     1.2 +++ b/src/HOL/Hyperreal/Fact.thy	Tue Oct 12 11:48:21 2004 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  header{*Factorial Function*}
     1.5  
     1.6  theory Fact
     1.7 -imports Real
     1.8 +imports "../Real/Real"
     1.9  begin
    1.10  
    1.11  consts fact :: "nat => nat"
     2.1 --- a/src/HOL/Hyperreal/SEQ.thy	Mon Oct 11 19:36:48 2004 +0200
     2.2 +++ b/src/HOL/Hyperreal/SEQ.thy	Tue Oct 12 11:48:21 2004 +0200
     2.3 @@ -1097,6 +1097,7 @@
     2.4  Goal "subseq f ==> \<exists>n. N1 \<le> n & N2 \<le> f(n)";
     2.5   ---------------------------------------------------------------***)
     2.6  
     2.7 +
     2.8  ML
     2.9  {*
    2.10  val Cauchy_def = thm"Cauchy_def";
    2.11 @@ -1214,15 +1215,8 @@
    2.12  val monoseq_realpow = thm "monoseq_realpow";
    2.13  val convergent_realpow = thm "convergent_realpow";
    2.14  val NSLIMSEQ_realpow_zero = thm "NSLIMSEQ_realpow_zero";
    2.15 -val LIMSEQ_realpow_zero = thm "LIMSEQ_realpow_zero";
    2.16 -val LIMSEQ_divide_realpow_zero = thm "LIMSEQ_divide_realpow_zero";
    2.17 -val LIMSEQ_rabs_realpow_zero = thm "LIMSEQ_rabs_realpow_zero";
    2.18 -val NSLIMSEQ_rabs_realpow_zero = thm "NSLIMSEQ_rabs_realpow_zero";
    2.19 -val LIMSEQ_rabs_realpow_zero2 = thm "LIMSEQ_rabs_realpow_zero2";
    2.20 -val NSLIMSEQ_rabs_realpow_zero2 = thm "NSLIMSEQ_rabs_realpow_zero2";
    2.21 -val NSBseq_HFinite_hypreal = thm "NSBseq_HFinite_hypreal";
    2.22 -val NSLIMSEQ_zero_Infinitesimal_hypreal = thm "NSLIMSEQ_zero_Infinitesimal_hypreal";
    2.23  *}
    2.24  
    2.25 +
    2.26  end
    2.27  
     3.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Mon Oct 11 19:36:48 2004 +0200
     3.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Tue Oct 12 11:48:21 2004 +0200
     3.3 @@ -2589,8 +2589,8 @@
     3.4        ==> \<exists>r. 0 < r & (\<forall>x. x \<noteq> c & \<bar>c - x\<bar> < r --> f x \<noteq> 0)"
     3.5  apply (cut_tac x = l and y = 0 in linorder_less_linear, auto)
     3.6  apply (drule LIM_fun_less_zero)
     3.7 -apply (drule_tac [3] LIM_fun_gt_zero, auto)
     3.8 -apply (rule_tac [!] x = r in exI, auto)
     3.9 +apply (drule_tac [3] LIM_fun_gt_zero)
    3.10 +apply force+
    3.11  done
    3.12  
    3.13  ML