src/ZF/ex/Limit.thy
changeset 79283 2c5d4b4ea3a2
parent 76216 9fc34f76b4e8