src/ZF/ind_syntax.ML
changeset 30153 051d3825a15d
parent 28965 1de908189869
child 30345 76fd85bbf139