src/HOL/ex/NatSum.ML
changeset 10168 50be659d4222
parent 8976 340d306f0118
child 10698 dc5e984dfe13