doc-src/Inductive/ind-defs.tex
changeset 12587 3f3d2ffb5df5
parent 9695 ec7d7f877712
child 42637 381fdcab0f36