src/ZF/ind_syntax.ML
changeset 12544 c78a00903e52
parent 12243 a2c0aaf94460
child 13150 0c50d13d449a