src/ZF/ex/NatSum.thy
changeset 15166 66f0584aa714
parent 12867 5c900a821a7c
child 16417 9bc16273c2d4