src/ZF/ind_syntax.ML
changeset 32890 77df12652210
parent 32765 3032c0308019
child 32952 aeb1e44fbc19