tuned comment;
authorwenzelm
Sun Nov 04 21:12:03 2001 +0100 (2001-11-04)
changeset 120506934c005aec4
parent 12049 58a2e6750d23
child 12051 650f854b7310
tuned comment;
src/HOL/thy_syntax.ML
src/ZF/thy_syntax.ML
     1.1 --- a/src/HOL/thy_syntax.ML	Sun Nov 04 21:00:28 2001 +0100
     1.2 +++ b/src/HOL/thy_syntax.ML	Sun Nov 04 21:12:03 2001 +0100
     1.3 @@ -2,7 +2,7 @@
     1.4      ID:         $Id$
     1.5      Author:     Markus Wenzel and Lawrence C Paulson and Carsten Clasohm
     1.6  
     1.7 -Additional theory file sections for HOL.
     1.8 +Additional sections for *old-style* theory files in HOL.
     1.9  *)
    1.10  
    1.11  local
     2.1 --- a/src/ZF/thy_syntax.ML	Sun Nov 04 21:00:28 2001 +0100
     2.2 +++ b/src/ZF/thy_syntax.ML	Sun Nov 04 21:12:03 2001 +0100
     2.3 @@ -3,13 +3,11 @@
     2.4      Author:     Lawrence C Paulson
     2.5      Copyright   1994  University of Cambridge
     2.6  
     2.7 -Additional theory file sections for ZF.
     2.8 +Additional sections for *old-style* theory files in ZF.
     2.9  *)
    2.10  
    2.11 -
    2.12  local
    2.13  
    2.14 -
    2.15  open ThyParse;
    2.16  
    2.17  (*ML identifiers for introduction rules.*)