# HG changeset patch
# User wenzelm
# Date 1165786026 -3600
# Node ID 12a2773e3608c56e9b09a15d60a0fe9cc0abe614
# Parent  c7ca3b57557fd48d1ed651dbf091fc1cf14fab5e
tuned comments;

diff -r c7ca3b57557f -r 12a2773e3608 src/HOL/Tools/numeral_syntax.ML
--- a/src/HOL/Tools/numeral_syntax.ML	Sun Dec 10 22:27:05 2006 +0100
+++ b/src/HOL/Tools/numeral_syntax.ML	Sun Dec 10 22:27:06 2006 +0100
@@ -2,8 +2,7 @@
     ID:         $Id$
     Authors:    Markus Wenzel, TU Muenchen
 
-Concrete syntax for generic numerals.  Assumes consts and syntax of
-theory HOL/Numeral.
+Concrete syntax for generic numerals.
 *)
 
 signature NUMERAL_SYNTAX =