src/ZF/equalities.thy
changeset 15222 2406fd8a5c30
parent 14883 ca000a495448
child 16417 9bc16273c2d4