src/HOL/Tools/numeral_syntax.ML
changeset 21763 12a2773e3608
parent 20094 99f27df2b6d0
child 21780 ec264b9daf94
     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 =