diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 6dbdaedd43..01816a3960 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1115,6 +1115,15 @@ the following way: \item {\tt H: A $\vd$ $\neg$B} \ becomes \ {\tt H: B $\vd$ $\neg$A} \end{itemize} +\subsection{\tt exfalso} +\label{exfalso} +\tacindex{exfalso} + +This tactic implements the ``ex falso quodlibet'' logical principle: +an elimination of {\tt False} is performed on the current goal, and the +user is then required to prove that {\tt False} is indeed provable in +the current context. This tactic is a macro for {\tt elimtype False}. + \section{Conversion tactics \index{Conversion tactics} \label{Conversion-tactics}} |