src/ZF/ind_syntax.ML
changeset 3843 162f95673705
parent 2266 82aef6857c5b
child 3925 90f499226ab9