src/HOL/Tools/numeral_syntax.ML
changeset 19295 c5d236fe9668
parent 18708 4b3dadb4fe33
child 19381 6cd8abc7f15b