src/HOL/Tools/numeral_syntax.ML
changeset 35144 8b8302da3a55
parent 35123 e286d5df187a
child 35363 09489d8ffece