src/HOL/Tools/numeral_syntax.ML
changeset 24749 151b3758f576
parent 24712 64ed05609568
child 25919 8b1c0d434824