src/HOL/Tools/numeral_syntax.ML
changeset 7497 a18f3bce7198
parent 7429 8f284fbb8728
child 7550 060f9954f73d