src/HOL/ZF/LProd.thy
changeset 34306 e8b8ee60c1e2
parent 29667 53103fc8ffa3
child 35416 d8d7d1b785af