src/ZF/ex/misc.thy
changeset 16913 1d8a8d010e69
parent 16417 9bc16273c2d4
child 17093 7e3828a6ebcc