src/HOL/Tools/numeral_syntax.ML
changeset 16123 1381e90c2694
parent 15965 f422f8283491
child 16365 838c65dad23a