src/ZF/ind_syntax.ML
changeset 47411 7df9a4f320a5
parent 44241 7943b69f0188
child 55143 04448228381d