src/ZF/ind_syntax.ML
changeset 613 f9eb0f819642
parent 578 efc648d29dd0
child 742 faa3efc1d130