src/HOL/ex/NatSum.thy
changeset 15958 b4ea8bf8e2f7
parent 15561 045a07ac35a7
child 16417 9bc16273c2d4