doc-src/Inductive/ind-defs.tex
changeset 24505 9e6d91f8bb73
parent 9695 ec7d7f877712
child 42637 381fdcab0f36
equal deleted inserted replaced
24504:0edc609e36fd 24505:9e6d91f8bb73