src/ZF/Induct/Brouwer.thy
changeset 62337 d3996d5873dd
parent 61980 6b780867d426
child 65449 c82e63b11b8b