src/ZF/ind_syntax.ML
changeset 5989 9670dae0143d
parent 4972 7fe1d30c1374
child 6053 8a1059aa01f0