src/HOL/ZF/LProd.thy
changeset 40815 6e2d17cc0d1d
parent 35422 e74b6f3b950c
child 41413 64cd30d6b0b8