src/ZF/ind_syntax.ML
changeset 22133 dd8a81e84a1c
parent 21539 c5cf9243ad62
child 22567 1565d476a9e2
equal deleted inserted replaced
22132:0f26cd597193 22133:dd8a81e84a1c