src/ZF/ind_syntax.ML
changeset 30925 c38cbc0ac8d1
parent 30345 76fd85bbf139
child 32740 9dd0a2f83429