src/ZF/ind-syntax.ML
changeset 7145 c05373eebee3
parent 70 8a29f8b4aca1