diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index d3d1ad918e..abc294e8b1 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1515,6 +1515,10 @@ equivalent to {\tt intros; apply ci}. case of existential quantification $\exists x\cdot P(x)$. Then, it is equivalent to {\tt intros; constructor 1 with \bindinglist}. +\item {\tt exists \nelist{\bindinglist}{,}} + + This iteratively applies {\tt exists {\bindinglist}}. + \item {\tt left}\tacindex{left}\\ {\tt right}\tacindex{right} |