src/ZF/ind_syntax.ML
changeset 3362 0b268cff9344
parent 2266 82aef6857c5b
child 3925 90f499226ab9