doc-src/Inductive/ind-defs.tex
changeset 3246 7f783705c7a4
parent 3162 78fa85d44e68
child 4239 8c98484ef66f