src/ZF/ind_syntax.ML
changeset 14722 8e739a6eaf11
parent 13150 0c50d13d449a
child 15570 8d8c70b41bab