src/HOL/Tools/numeral_syntax.ML
changeset 10168 50be659d4222
parent 9314 fd8b0f219879
child 10693 9e4a0e84d0d6