src/HOL/Hyperreal/SEQ.thy
changeset 13810 c3fbfd472365
parent 12018 ec054019c910
child 15082 6c3276a2735b
     1.1 --- a/src/HOL/Hyperreal/SEQ.thy	Fri Feb 07 15:36:54 2003 +0100
     1.2 +++ b/src/HOL/Hyperreal/SEQ.thy	Fri Feb 07 16:40:23 2003 +0100
     1.3 @@ -14,7 +14,7 @@
     1.4    
     1.5    (* Nonstandard definition of convergence of sequence *)
     1.6    NSLIMSEQ :: [nat=>real,real] => bool    ("((_)/ ----NS> (_))" [60, 60] 60)
     1.7 -  "X ----NS> L == (ALL N: HNatInfinite. (*fNat* X) N @= hypreal_of_real L)"
     1.8 +  "X ----NS> L == (ALL N: HNatInfinite. ( *fNat* X) N @= hypreal_of_real L)"
     1.9  
    1.10    (* define value of limit using choice operator*)
    1.11    lim :: (nat => real) => real
    1.12 @@ -37,7 +37,7 @@
    1.13   
    1.14    (* Nonstandard definition for bounded sequence *)
    1.15    NSBseq :: (nat=>real) => bool
    1.16 -  "NSBseq X == (ALL N: HNatInfinite. (*fNat* X) N : HFinite)" 
    1.17 +  "NSBseq X == (ALL N: HNatInfinite. ( *fNat* X) N : HFinite)" 
    1.18  
    1.19    (* Definition for monotonicity *)
    1.20    monoseq :: (nat=>real)=>bool
    1.21 @@ -58,6 +58,6 @@
    1.22  
    1.23    NSCauchy :: (nat => real) => bool
    1.24    "NSCauchy X == (ALL M: HNatInfinite. ALL N: HNatInfinite.
    1.25 -                      (*fNat* X) M @= (*fNat* X) N)"
    1.26 +                      ( *fNat* X) M @= ( *fNat* X) N)"
    1.27  end
    1.28