src/ZF/ex/contract0.thy
changeset 7370 6407a09ac58f
parent 16 0b033d50ca1c