src/ZF/ind_syntax.ML
changeset 36135 89d1903fbd50
parent 35129 ed24ba6f69aa
child 37145 01aa36932739