# HG changeset patch
# User wenzelm
# Date 1003337550 -7200
# Node ID 9283b3c11234863afe434e4ded7b4a5b9a3cb991
# Parent  9eab353e810b975466cf64cd72c4647cc00a6e4a
tuned comments;

diff -r 9eab353e810b -r 9283b3c11234 src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Wed Oct 17 18:51:03 2001 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Wed Oct 17 18:52:30 2001 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/Thy/thm_deps.ML
     ID:         $Id$
     Author:     Stefan Berghofer, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Visualize dependencies of theorems.
 *)
diff -r 9eab353e810b -r 9283b3c11234 src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Wed Oct 17 18:51:03 2001 +0200
+++ b/src/Pure/Thy/thy_parse.ML	Wed Oct 17 18:52:30 2001 +0200
@@ -1,8 +1,9 @@
 (*  Title:      Pure/Thy/thy_parse.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-The parser for theory files.
+The parser for *old-style* theory files.
 *)
 
 infix 5 -- --$$ $$-- ^^;
diff -r 9eab353e810b -r 9283b3c11234 src/Pure/Thy/thy_scan.ML
--- a/src/Pure/Thy/thy_scan.ML	Wed Oct 17 18:51:03 2001 +0200
+++ b/src/Pure/Thy/thy_scan.ML	Wed Oct 17 18:52:30 2001 +0200
@@ -1,8 +1,9 @@
 (*  Title:	Pure/Thy/thy_scan.ML
     ID:		$Id$
     Author:	Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-Lexer for the outer Isabelle syntax.
+Lexer for *old-style* outer syntax.
 *)
 
 signature THY_SCAN =
diff -r 9eab353e810b -r 9283b3c11234 src/Pure/Thy/thy_syn.ML
--- a/src/Pure/Thy/thy_syn.ML	Wed Oct 17 18:51:03 2001 +0200
+++ b/src/Pure/Thy/thy_syn.ML	Wed Oct 17 18:52:30 2001 +0200
@@ -1,8 +1,9 @@
 (*  Title:      Pure/Thy/thy_syn.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-Provide syntax for old-style theory files.
+Provide syntax for *old-style* theory files.
 *)
 
 signature BASIC_THY_SYN =
diff -r 9eab353e810b -r 9283b3c11234 src/Pure/context.ML
--- a/src/Pure/context.ML	Wed Oct 17 18:51:03 2001 +0200
+++ b/src/Pure/context.ML	Wed Oct 17 18:52:30 2001 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/context.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Global theory context.
 *)