src/HOL/Tools/numeral_syntax.ML
changeset 24699 c6674504103f
parent 24630 351a308ab58d
child 24712 64ed05609568
equal deleted inserted replaced
24698:9800a7602629 24699:c6674504103f