src/HOL/ex/NatSum.thy
changeset 76371 1ac2416e8432
parent 68224 1f7308050349