src/ZF/ex/misc.thy
changeset 81726 27ba0fed2071
parent 80777 623d46973cbe