src/ZF/ind_syntax.ML
changeset 52477 025b3777e592
parent 44241 7943b69f0188
child 55143 04448228381d