src/ZF/ind_syntax.ML
changeset 80408 e6d3d1db6136
parent 74375 ba880f3a4e52