src/ZF/ind-syntax.ML
changeset 13016 c039b8ede204
parent 70 8a29f8b4aca1