src/ZF/ind_syntax.ML
changeset 4054 b33e02b3478e
parent 3925 90f499226ab9
child 4352 7ac9f3e8a97d