src/ZF/ind_syntax.ML
changeset 21889 682dbe947862
parent 21539 c5cf9243ad62
child 22567 1565d476a9e2