src/ZF/ind_syntax.ML
changeset 3196 c522bc46aea7
parent 2266 82aef6857c5b
child 3925 90f499226ab9
equal deleted inserted replaced
3195:dcb458d38724 3196:c522bc46aea7