src/ZF/ind-syntax.ML
changeset 5951 e98c900540f9
parent 70 8a29f8b4aca1