src/ZF/ind_syntax.ML
changeset 1858 513316fd1087
parent 1738 a70a5bc5e315
child 2226 f3c6a22681b1