src/HOL/Tools/numeral_syntax.ML
changeset 25571 c9e39eafc7a0
parent 24712 64ed05609568
child 25919 8b1c0d434824
equal deleted inserted replaced
25570:fdfbbb92dadf 25571:c9e39eafc7a0