src/HOL/ZF/LProd.thy
changeset 82775 61c39a9e5415
parent 67613 ce654b0e6d69