src/ZF/Sum.thy
changeset 35655 e8e4af6da819
parent 35416 d8d7d1b785af
child 38514 bd9c4e8281ec