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