src/ZF/ind_syntax.ML
changeset 2414 13df7d6c5c3b
parent 2266 82aef6857c5b
child 3925 90f499226ab9