src/ZF/ind_syntax.ML
changeset 32911 5f7386f7cbe6
parent 32765 3032c0308019
child 32952 aeb1e44fbc19