src/ZF/ind_syntax.ML
changeset 6374 a67e4729efb2
parent 6112 5e4871c5136b
child 7694 20121c9dc1a6