src/HOL/Tools/numeral_syntax.ML
changeset 7165 8c937127fd8c
parent 7078 4e64b2bd10ce
child 7429 8f284fbb8728