src/HOL/Hyperreal/SEQ.ML
changeset 13810 c3fbfd472365
parent 12486 0ed8bdd883e0
child 14268 5cf13e80be0e
     1.1 --- a/src/HOL/Hyperreal/SEQ.ML	Fri Feb 07 15:36:54 2003 +0100
     1.2 +++ b/src/HOL/Hyperreal/SEQ.ML	Fri Feb 07 16:40:23 2003 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4   -------------------------------------------------------------------------- *)
     1.5  
     1.6  Goalw [hypnat_omega_def] 
     1.7 -      "(*fNat* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal";
     1.8 +      "( *fNat* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal";
     1.9  by (auto_tac (claset(),
    1.10        simpset() addsimps [Infinitesimal_FreeUltrafilterNat_iff,starfunNat]));
    1.11  by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
    1.12 @@ -31,7 +31,7 @@
    1.13  qed "LIMSEQ_iff";
    1.14  
    1.15  Goalw [NSLIMSEQ_def] 
    1.16 -    "(X ----NS> L) = (ALL N: HNatInfinite. (*fNat* X) N @= hypreal_of_real L)";
    1.17 +    "(X ----NS> L) = (ALL N: HNatInfinite. ( *fNat* X) N @= hypreal_of_real L)";
    1.18  by (Simp_tac 1);
    1.19  qed "NSLIMSEQ_iff";
    1.20  
    1.21 @@ -121,7 +121,7 @@
    1.22  val lemmaLIM2 = result();
    1.23  
    1.24  Goal "[| 0 < r; ALL n. r <= abs (X (f n) + - L); \
    1.25 -\          (*fNat* X) (Abs_hypnat (hypnatrel `` {f})) + \
    1.26 +\          ( *fNat* X) (Abs_hypnat (hypnatrel `` {f})) + \
    1.27  \          - hypreal_of_real  L @= 0 |] ==> False";
    1.28  by (auto_tac (claset(),simpset() addsimps [starfunNat,
    1.29      mem_infmal_iff RS sym,hypreal_of_real_def,
    1.30 @@ -419,12 +419,12 @@
    1.31  qed "Bseq_iff1a";
    1.32  
    1.33  Goalw [NSBseq_def]
    1.34 -     "[| NSBseq X;  N: HNatInfinite |] ==> (*fNat* X) N : HFinite";
    1.35 +     "[| NSBseq X;  N: HNatInfinite |] ==> ( *fNat* X) N : HFinite";
    1.36  by (Blast_tac 1);
    1.37  qed "NSBseqD";
    1.38  
    1.39  Goalw [NSBseq_def]
    1.40 -     "ALL N: HNatInfinite. (*fNat* X) N : HFinite ==> NSBseq X";
    1.41 +     "ALL N: HNatInfinite. ( *fNat* X) N : HFinite ==> NSBseq X";
    1.42  by (assume_tac 1);
    1.43  qed "NSBseqI";
    1.44