src/ZF/Finite.thy
changeset 33318 ddd97d9dfbfb
parent 32960 69916a850301
child 45602 2a858377c3d2