src/HOL/Real/Hyperreal/SEQ.thy
changeset 10648 a8c647cfa31f
parent 10045 c76b73e16711
     1.1 --- a/src/HOL/Real/Hyperreal/SEQ.thy	Tue Dec 12 11:59:25 2000 +0100
     1.2 +++ b/src/HOL/Real/Hyperreal/SEQ.thy	Tue Dec 12 12:01:19 2000 +0100
     1.3 @@ -9,11 +9,11 @@
     1.4  constdefs
     1.5  
     1.6    (* Standard definition of convergence of sequence *)           
     1.7 -  LIMSEQ :: [nat=>real,real] => bool    ("((_)/ ----> (_))" 60)
     1.8 +  LIMSEQ :: [nat=>real,real] => bool    ("((_)/ ----> (_))" [60, 60] 60)
     1.9    "X ----> L == (ALL r. #0 < r --> (EX no. ALL n. no <= n --> abs (X n + -L) < r))"
    1.10    
    1.11    (* Nonstandard definition of convergence of sequence *)
    1.12 -  NSLIMSEQ :: [nat=>real,real] => bool    ("((_)/ ----NS> (_))" 60)
    1.13 +  NSLIMSEQ :: [nat=>real,real] => bool    ("((_)/ ----NS> (_))" [60, 60] 60)
    1.14    "X ----NS> L == (ALL N: HNatInfinite. (*fNat* X) N @= hypreal_of_real L)"
    1.15  
    1.16    (* define value of limit using choice operator*)