doc-src/Inductive/ind-defs.tex
changeset 42739 017e5dac8642
parent 42637 381fdcab0f36