src/HOL/Tools/numeral_syntax.ML
changeset 16240 95cc0e8f8a17
parent 15965 f422f8283491
child 16365 838c65dad23a