src/HOL/Tools/numeral_syntax.ML
changeset 9230 17ae63f82ad8
parent 7550 060f9954f73d
child 9314 fd8b0f219879
equal deleted inserted replaced
9229:a7c6ea7e57de 9230:17ae63f82ad8
     1 (*  Title:      HOL/Tools/numeral_syntax.ML
     1 (*  Title:      HOL/Tools/numeral_syntax.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     3     Author:     Markus Wenzel, TU Muenchen
       
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     4 
     5 
     5 Concrete syntax for generic numerals.  Assumes consts and syntax of
     6 Concrete syntax for generic numerals.  Assumes consts and syntax of
     6 theory HOL/Numeral.
     7 theory HOL/Numeral.
     7 *)
     8 *)
     8 
     9