src/HOL/Tools/numeral_syntax.ML
changeset 32318 bca7fd849829
parent 29316 0a7fcdd77f4b
child 35115 446c5063e4fd
equal deleted inserted replaced
32317:b4b871808223 32318:bca7fd849829