src/HOL/Tools/numeral_syntax.ML
changeset 15341 254f6f00b60e
parent 15013 34264f5e4691
child 15595 dc8a41c7cefc