src/HOL/Tools/numeral_syntax.ML
changeset 29270 0eade173f77e
parent 26086 3c243098b64a
child 29316 0a7fcdd77f4b