src/ZF/Sum.thy
changeset 38343 e5418eec375c
parent 35416 d8d7d1b785af
child 38514 bd9c4e8281ec