src/ZF/Sum.thy
changeset 13605 528f7489a403
parent 13356 c9cfe1638bf2
child 13823 d49ffd9f9662