# HG changeset patch
# User huffman
# Date 1126895444 -7200
# Node ID a358da1a021851b530d0e7e8474e6147cfef4770
# Parent  e40afa46107877e3d75656f5c5b7e5e8a0a41640
add header

diff -r e40afa461078 -r a358da1a0218 src/HOL/Hyperreal/SEQ.thy
--- a/src/HOL/Hyperreal/SEQ.thy	Fri Sep 16 16:07:22 2005 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy	Fri Sep 16 20:30:44 2005 +0200
@@ -6,6 +6,8 @@
     Additional contributions by Jeremy Avigad
 *)
 
+header {* Sequences and Series *}
+
 theory SEQ
 imports NatStar
 begin