src/ZF/Sum.thy
changeset 45379 0147a4348ca1
parent 41777 1f7cbe39d425
child 45602 2a858377c3d2