src/ZF/ind_syntax.ML
changeset 777 c007eba368b7
parent 742 faa3efc1d130
child 1418 f5f97ee67cbb