src/HOL/ex/NatSum.ML
changeset 4479 708d7c26db5b
parent 4246 c539e702e1d2
child 4558 31becfd8d329