src/ZF/ind_syntax.ML
changeset 15740 d63e7a65b2d0
parent 15570 8d8c70b41bab
child 16867 cf7d61d56acf