# HG changeset patch
# User wenzelm
# Date 1112858778 -7200
# Node ID 6e6233e8cf5e84558c6e0c07a2587dbd05bbecc7
# Parent  7e3bee7df06e036beace6ffdf0cd90b772af984f
added header;

diff -r 7e3bee7df06e -r 6e6233e8cf5e src/Pure/General/lazy_scan.ML
--- a/src/Pure/General/lazy_scan.ML	Thu Apr 07 09:26:10 2005 +0200
+++ b/src/Pure/General/lazy_scan.ML	Thu Apr 07 09:26:18 2005 +0200
@@ -1,4 +1,9 @@
-(* $Id$ *)
+(*  Title:      Pure/General/lazy_scan.ML
+    ID:         $Id$
+    Author:     Sebastian Skalberg, TU Muenchen
+
+Scanner combinators for lazy sequences.
+*)
 
 signature LAZY_SCAN =
 sig
diff -r 7e3bee7df06e -r 6e6233e8cf5e src/Pure/General/lazy_seq.ML
--- a/src/Pure/General/lazy_seq.ML	Thu Apr 07 09:26:10 2005 +0200
+++ b/src/Pure/General/lazy_seq.ML	Thu Apr 07 09:26:18 2005 +0200
@@ -1,3 +1,10 @@
+(*  Title:      Pure/General/lazy_seq.ML
+    ID:         $Id$
+    Author:     Sebastian Skalberg, TU Muenchen
+
+Alternative version of lazy sequences.
+*)
+
 signature LAZY_SEQ =
 sig