src/ZF/ind_syntax.ML
changeset 5973 040f6d2af50d
parent 4972 7fe1d30c1374
child 6053 8a1059aa01f0