src/ZF/ind_syntax.ML
changeset 17740 fc385ce6187d
parent 16867 cf7d61d56acf
child 17988 47f81afce1b4