src/HOL/Hyperreal/SEQ.thy
changeset 17439 a358da1a0218
parent 17429 e8d6ed3aacfe
child 18585 5d379fe2eb74
     1.1 --- a/src/HOL/Hyperreal/SEQ.thy	Fri Sep 16 16:07:22 2005 +0200
     1.2 +++ b/src/HOL/Hyperreal/SEQ.thy	Fri Sep 16 20:30:44 2005 +0200
     1.3 @@ -6,6 +6,8 @@
     1.4      Additional contributions by Jeremy Avigad
     1.5  *)
     1.6  
     1.7 +header {* Sequences and Series *}
     1.8 +
     1.9  theory SEQ
    1.10  imports NatStar
    1.11  begin