src/HOL/ex/NatSum.thy
changeset 55595 2e2e9bc7c4c6
parent 54703 499f92dc6e45
child 58770 ae5e9b4f8daf