src/ZF/ex/NatSum.thy
changeset 25577 d739f48ef40c
parent 16417 9bc16273c2d4
child 35762 af3ff2ba4c54