src/ZF/ind_syntax.ML
changeset 22133 dd8a81e84a1c
parent 21539 c5cf9243ad62
child 22567 1565d476a9e2