src/ZF/ind_syntax.ML
changeset 17459 9a3925c07392
parent 16867 cf7d61d56acf
child 17988 47f81afce1b4