src/HOL/ZF/LProd.thy
changeset 20977 dbf1eca9b34e
parent 19769 c40ce2de2020
child 22282 71b4aefad227