src/ZF/ind_syntax.ML
changeset 5480 93c21fee39f8
parent 4972 7fe1d30c1374
child 6053 8a1059aa01f0