src/ZF/ind_syntax.ML
changeset 24339 d929e9b2e598
parent 23419 8c30dd4b3b22
child 24826 78e6a3cea367