src/HOL/ZF/LProd.thy
changeset 39444 beabb8443ee4
parent 35422 e74b6f3b950c
child 41413 64cd30d6b0b8