src/ZF/ind_syntax.ML
changeset 20153 6ff5d35749b0
parent 18176 ae9bd644d106
child 21539 c5cf9243ad62