src/ZF/ind_syntax.ML
changeset 19154 f48e36b7d8d4
parent 18176 ae9bd644d106
child 21539 c5cf9243ad62