doc-src/Inductive/ind-defs.tex
changeset 3362 0b268cff9344
parent 3162 78fa85d44e68
child 4239 8c98484ef66f