src/HOL/Hyperreal/SEQ.thy
changeset 15241 a3949068537e
parent 15236 f289e8ba2bb3
child 15251 bb6f072c8d10
     1.1 --- a/src/HOL/Hyperreal/SEQ.thy	Mon Oct 11 19:36:48 2004 +0200
     1.2 +++ b/src/HOL/Hyperreal/SEQ.thy	Tue Oct 12 11:48:21 2004 +0200
     1.3 @@ -1097,6 +1097,7 @@
     1.4  Goal "subseq f ==> \<exists>n. N1 \<le> n & N2 \<le> f(n)";
     1.5   ---------------------------------------------------------------***)
     1.6  
     1.7 +
     1.8  ML
     1.9  {*
    1.10  val Cauchy_def = thm"Cauchy_def";
    1.11 @@ -1214,15 +1215,8 @@
    1.12  val monoseq_realpow = thm "monoseq_realpow";
    1.13  val convergent_realpow = thm "convergent_realpow";
    1.14  val NSLIMSEQ_realpow_zero = thm "NSLIMSEQ_realpow_zero";
    1.15 -val LIMSEQ_realpow_zero = thm "LIMSEQ_realpow_zero";
    1.16 -val LIMSEQ_divide_realpow_zero = thm "LIMSEQ_divide_realpow_zero";
    1.17 -val LIMSEQ_rabs_realpow_zero = thm "LIMSEQ_rabs_realpow_zero";
    1.18 -val NSLIMSEQ_rabs_realpow_zero = thm "NSLIMSEQ_rabs_realpow_zero";
    1.19 -val LIMSEQ_rabs_realpow_zero2 = thm "LIMSEQ_rabs_realpow_zero2";
    1.20 -val NSLIMSEQ_rabs_realpow_zero2 = thm "NSLIMSEQ_rabs_realpow_zero2";
    1.21 -val NSBseq_HFinite_hypreal = thm "NSBseq_HFinite_hypreal";
    1.22 -val NSLIMSEQ_zero_Infinitesimal_hypreal = thm "NSLIMSEQ_zero_Infinitesimal_hypreal";
    1.23  *}
    1.24  
    1.25 +
    1.26  end
    1.27