doc-src/Inductive/ind-defs.tex
changeset 7990 0a604b2fc2b1
parent 7829 c2672c537894
child 9695 ec7d7f877712