tuned comments;
authorwenzelm
Wed Oct 17 18:52:30 2001 +0200 (2001-10-17)
changeset 118199283b3c11234
parent 11818 9eab353e810b
child 11820 015a82d4ee96
tuned comments;
src/Pure/Thy/thm_deps.ML
src/Pure/Thy/thy_parse.ML
src/Pure/Thy/thy_scan.ML
src/Pure/Thy/thy_syn.ML
src/Pure/context.ML
     1.1 --- a/src/Pure/Thy/thm_deps.ML	Wed Oct 17 18:51:03 2001 +0200
     1.2 +++ b/src/Pure/Thy/thm_deps.ML	Wed Oct 17 18:52:30 2001 +0200
     1.3 @@ -1,6 +1,7 @@
     1.4  (*  Title:      Pure/Thy/thm_deps.ML
     1.5      ID:         $Id$
     1.6      Author:     Stefan Berghofer, TU Muenchen
     1.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.8  
     1.9  Visualize dependencies of theorems.
    1.10  *)
     2.1 --- a/src/Pure/Thy/thy_parse.ML	Wed Oct 17 18:51:03 2001 +0200
     2.2 +++ b/src/Pure/Thy/thy_parse.ML	Wed Oct 17 18:52:30 2001 +0200
     2.3 @@ -1,8 +1,9 @@
     2.4  (*  Title:      Pure/Thy/thy_parse.ML
     2.5      ID:         $Id$
     2.6      Author:     Markus Wenzel, TU Muenchen
     2.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     2.8  
     2.9 -The parser for theory files.
    2.10 +The parser for *old-style* theory files.
    2.11  *)
    2.12  
    2.13  infix 5 -- --$$ $$-- ^^;
     3.1 --- a/src/Pure/Thy/thy_scan.ML	Wed Oct 17 18:51:03 2001 +0200
     3.2 +++ b/src/Pure/Thy/thy_scan.ML	Wed Oct 17 18:52:30 2001 +0200
     3.3 @@ -1,8 +1,9 @@
     3.4  (*  Title:	Pure/Thy/thy_scan.ML
     3.5      ID:		$Id$
     3.6      Author:	Markus Wenzel, TU Muenchen
     3.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     3.8  
     3.9 -Lexer for the outer Isabelle syntax.
    3.10 +Lexer for *old-style* outer syntax.
    3.11  *)
    3.12  
    3.13  signature THY_SCAN =
     4.1 --- a/src/Pure/Thy/thy_syn.ML	Wed Oct 17 18:51:03 2001 +0200
     4.2 +++ b/src/Pure/Thy/thy_syn.ML	Wed Oct 17 18:52:30 2001 +0200
     4.3 @@ -1,8 +1,9 @@
     4.4  (*  Title:      Pure/Thy/thy_syn.ML
     4.5      ID:         $Id$
     4.6      Author:     Markus Wenzel, TU Muenchen
     4.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     4.8  
     4.9 -Provide syntax for old-style theory files.
    4.10 +Provide syntax for *old-style* theory files.
    4.11  *)
    4.12  
    4.13  signature BASIC_THY_SYN =
     5.1 --- a/src/Pure/context.ML	Wed Oct 17 18:51:03 2001 +0200
     5.2 +++ b/src/Pure/context.ML	Wed Oct 17 18:52:30 2001 +0200
     5.3 @@ -1,6 +1,7 @@
     5.4  (*  Title:      Pure/context.ML
     5.5      ID:         $Id$
     5.6      Author:     Markus Wenzel, TU Muenchen
     5.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5.8  
     5.9  Global theory context.
    5.10  *)