src/ZF/ind_syntax.ML
changeset 39657 5e57675b7e40
parent 39288 f1ae2493d93f
child 41310 65631ca437c9