src/HOL/Tools/numeral_syntax.ML
changeset 9950 879e88b1e552
parent 9314 fd8b0f219879
child 10693 9e4a0e84d0d6