src/HOL/Tools/numeral_syntax.ML
changeset 19402 742b7934ccfc
parent 19381 6cd8abc7f15b
child 19481 a6205c6203ea