src/HOL/ex/NatSum.thy
changeset 39133 70d3915c92f0
parent 28952 15a4b2cf8c34
child 40077 c8a9eaaa2f59