src/HOL/Tools/numeral_syntax.ML
changeset 13145 59bc43b51aa2
parent 13110 ca8cd110f769
child 13491 ddf6ae639f21