--- 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.
*)
--- 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 -- --$$ $$-- ^^;
--- 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 =
--- 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 =
--- 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.
*)