src/ZF/ind_syntax.ML
changeset 17357 ee2bdca144c7
parent 16867 cf7d61d56acf
child 17988 47f81afce1b4