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