src/ZF/ind_syntax.ML
changeset 45797 977cf00fb8d3
parent 44241 7943b69f0188
child 55143 04448228381d