src/HOL/Tools/numeral_syntax.ML
changeset 46834 a5fa1dc55945
parent 46236 ae79f2978a67
equal deleted inserted replaced
46833:85619a872ab5 46834:a5fa1dc55945