src/HOL/NSA/HSEQ.thy
changeset 58878 f962e42e324d
parent 54230 b1d955791529
child 61284 2314c2f62eb1
equal deleted inserted replaced
58877:262572d90bc6 58878:f962e42e324d
     4     Description : Convergence of sequences and series
     4     Description : Convergence of sequences and series
     5     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     5     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     6     Additional contributions by Jeremy Avigad and Brian Huffman
     6     Additional contributions by Jeremy Avigad and Brian Huffman
     7 *)
     7 *)
     8 
     8 
     9 header {* Sequences and Convergence (Nonstandard) *}
     9 section {* Sequences and Convergence (Nonstandard) *}
    10 
    10 
    11 theory HSEQ
    11 theory HSEQ
    12 imports Limits NatStar
    12 imports Limits NatStar
    13 begin
    13 begin
    14 
    14