src/HOL/ex/NatSum.thy
changeset 63386 0d6adf2d5035
parent 62348 9a5f43dac883
child 63680 6e1e8b5abbfa