src/HOL/Tools/numeral_syntax.ML
changeset 13249 4b3de6370184
parent 13110 ca8cd110f769
child 13491 ddf6ae639f21