src/ZF/ind_syntax.ML
changeset 29554 7e5e5ebb7bf7
parent 28965 1de908189869
child 30345 76fd85bbf139