doc-src/Inductive/ind-defs.tex
changeset 4576 be6b5edbca9f
parent 4265 70fc6e05120c
child 6124 3aa7926f039a