diff options
| author | jnarboux | 2006-06-09 16:29:01 +0000 |
|---|---|---|
| committer | jnarboux | 2006-06-09 16:29:01 +0000 |
| commit | 2b35ffb42735b9e3af78b06a01d18610fb1f3f97 (patch) | |
| tree | 2eae1ddefb10fae3d8f3d2472dd3e53c8321891d | |
| parent | 4ef543b711e2e066c8e3378667371ba4c7c5099b (diff) | |
ajout de la doc de classical_right et left
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8938 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 1663b975ab..4946be8f22 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -2108,6 +2108,17 @@ datatype: see~\ref{quote-examples} for the full details. % En attente d'un moyen de valoriser les fichiers de demos % \SeeAlso file \texttt{theories/DEMOS/DemoQuote.v} in the distribution +\section{Classical tactics} +\label{ClassicalTactics} + +In order to ease the proving process, when the {\tt Classical} module is loaded. A few more tactics are available. Make sure to load the module using the \texttt{Require Import} command. + +\subsection{{\tt classical\_left, classical\_right} \tacindex{classical\_left} \tacindex{classical\_right}} + +The tactics \texttt{classical\_left} and \texttt{classical\_right} are the analog of the \texttt{left} and \texttt{right} but using classical logic. They can only be used for disjunctions. +Use \texttt{classical\_left} to prove the left part of the disjunction with the assumption that the negation of right part holds. +Use \texttt{classical\_left} to prove the right part of the disjunction with the assumption that the negation of left part holds. + \section{Automatizing \label{Automatizing}} |