src/HOL/Tools/numeral_syntax.ML
changeset 25773 0d585d756745
parent 24712 64ed05609568
child 25919 8b1c0d434824