src/ZF/ind_syntax.ML
changeset 41107 8795cd75965e
parent 39288 f1ae2493d93f
child 41310 65631ca437c9