src/ZF/ind_syntax.ML
changeset 5769 6a422b22ba02
parent 4972 7fe1d30c1374
child 6053 8a1059aa01f0