src/HOL/Tools/numeral.ML
changeset 79531 22a137a6de44
parent 77879 dd222e2af01a
child 82380 ceb4f33d3073
equal deleted inserted replaced
79530:1b0fc6ceb750 79531:22a137a6de44