src/ZF/Finite.thy
changeset 81133 072cc2a92ba3
parent 80917 2a77bc3b4eac