src/ZF/ex/Rmap.thy
changeset 4227 a5c947d7c56c
parent 3841 22bbc1676768
child 11316 b4e71bd751e4