doc-src/Inductive/ind-defs.tex
changeset 48295 e0cf12269e60
parent 42637 381fdcab0f36