src/ZF/ind_syntax.ML
changeset 7636 102a4b6b83a6
parent 6112 5e4871c5136b
child 7694 20121c9dc1a6