doc-src/Inductive/ind-defs.tex
changeset 3701 6f0ed3eef1a9
parent 3162 78fa85d44e68
child 4239 8c98484ef66f