src/ZF/ind_syntax.ML
changeset 20810 3377a830b727
parent 18176 ae9bd644d106
child 21539 c5cf9243ad62