src/ZF/ind_syntax.ML
changeset 57978 8f4a332500e4
parent 55151 f331472f1027
child 59755 f8d164ab0dc1