src/ZF/ind_syntax.ML
changeset 13253 edbf32029d33
parent 13150 0c50d13d449a
child 15570 8d8c70b41bab
equal deleted inserted replaced
13252:8c79a0dce4c0 13253:edbf32029d33