src/HOL/ex/NatSum.thy
changeset 18608 9cdcc2a5c8b3
parent 16993 2ec0b8159e8e
child 21144 17b0b4c6491b