src/ZF/ind_syntax.ML
changeset 15270 8b3f707a78a7
parent 13150 0c50d13d449a
child 15570 8d8c70b41bab