src/HOL/ZF/LProd.thy
changeset 62462 c7def2433a06
parent 60515 484559628038
child 62651 66568c9b8216