src/ZF/Finite.thy
changeset 14722 8e739a6eaf11
parent 13784 b9f6154427a4
child 14883 ca000a495448