doc-src/Inductive/ind-defs.tex
changeset 4072 d0d32dd77440
parent 3162 78fa85d44e68
child 4239 8c98484ef66f