tuned comments;
authorwenzelm
Sun Dec 10 22:27:06 2006 +0100 (2006-12-10)
changeset 2176312a2773e3608
parent 21762 c7ca3b57557f
child 21764 720b0add5206
tuned comments;
src/HOL/Tools/numeral_syntax.ML
     1.1 --- a/src/HOL/Tools/numeral_syntax.ML	Sun Dec 10 22:27:05 2006 +0100
     1.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Sun Dec 10 22:27:06 2006 +0100
     1.3 @@ -2,8 +2,7 @@
     1.4      ID:         $Id$
     1.5      Authors:    Markus Wenzel, TU Muenchen
     1.6  
     1.7 -Concrete syntax for generic numerals.  Assumes consts and syntax of
     1.8 -theory HOL/Numeral.
     1.9 +Concrete syntax for generic numerals.
    1.10  *)
    1.11  
    1.12  signature NUMERAL_SYNTAX =