doc-src/Inductive/ind-defs.tex
changeset 47501 0b9294e093db
parent 42637 381fdcab0f36