src/ZF/Sum.thy
changeset 3631 88a279998f90
parent 2469 b50b8c0eec01
child 3923 c257b82a1200