diff options
Diffstat (limited to 'doc/refman/RefMan-tac.tex')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 52f32d0c7..2eebac18e 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1439,18 +1439,6 @@ a hypothesis or in the body or the type of a local definition. \end{Variants} -\subsection{\tt admit} -\tacindex{admit} -\label{admit} - -The {\tt admit} tactic ``solves'' the current subgoal by an -axiom. This typically allows temporarily skipping a subgoal so as to -progress further in the rest of the proof. To know if some proof still -relies on unproved subgoals, one can use the command {\tt Print -Assumptions} (see Section~\ref{PrintAssumptions}). Admitted subgoals -have names of the form {\ident}\texttt{\_admitted} possibly followed -by a number. - \subsection{\tt absurd \term} \tacindex{absurd} \label{absurd} |