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