src/HOL/Tools/numeral_syntax.ML
changeset 19295 c5d236fe9668
parent 18708 4b3dadb4fe33
child 19381 6cd8abc7f15b
equal deleted inserted replaced
19294:871d7aea081a 19295:c5d236fe9668