src/HOL/ex/NatSum.thy
changeset 17860 b4cf247ea0d2
parent 16993 2ec0b8159e8e
child 21144 17b0b4c6491b