src/ZF/ind_syntax.ML
changeset 12725 7ede865e1fe5
parent 12243 a2c0aaf94460
child 13150 0c50d13d449a