src/HOL/Tools/numeral_syntax.ML
changeset 35437 fe196f61b970
parent 35363 09489d8ffece
child 35430 df2862dc23a8
equal deleted inserted replaced
35422:e74b6f3b950c 35437:fe196f61b970