src/HOL/ex/NatSum.thy
changeset 8421 7156b8e26a17
parent 8356 14d89313c66c
child 8836 32fe62227ff0