src/ZF/ex/contract0.thy
changeset 8302 da404f79c1fc
parent 16 0b033d50ca1c