src/ZF/Sum.thy
changeset 72152 3fa75db844f5
parent 69593 3dda49e08b9d
child 76213 e44d86131648