src/ZF/ind_syntax.ML
changeset 4102 f746af27164b
parent 3925 90f499226ab9
child 4352 7ac9f3e8a97d
equal deleted inserted replaced
4101:e8ad51c88be9 4102:f746af27164b