src/ZF/Induct/Brouwer.thy
changeset 78832 c62003e05e46
parent 76215 a642599ffdea