src/ZF/ind_syntax.ML
changeset 2045 ae1030e66745
parent 1738 a70a5bc5e315
child 2226 f3c6a22681b1