src/ZF/ind_syntax.ML
changeset 12544 c78a00903e52
parent 12243 a2c0aaf94460
child 13150 0c50d13d449a
equal deleted inserted replaced
12543:3e355f0f079f 12544:c78a00903e52