diff options
| author | Julien Forest | 2014-04-04 22:06:16 +0200 |
|---|---|---|
| committer | Julien Forest | 2014-04-04 22:07:05 +0200 |
| commit | a324162435df4666be99a3872717c84d93cca5ce (patch) | |
| tree | af15e4370fb2a5bcf209939b7b0c9ef34fb9db4c | |
| parent | 3a80af7d4d69927af25ed45fa45a6320d8716a80 (diff) | |
fixing Function doc
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 89d8df473b..7b09d84637 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1920,7 +1920,7 @@ dependent induction and an explanation of the underlying technique. \tacindex{functional induction} \label{FunInduction} -The \emph{experimental} tactic \texttt{functional induction} performs +The tactic \texttt{functional induction} performs case analysis and induction following the definition of a function. It makes use of a principle generated by \texttt{Function} (see Section~\ref{Function}) or \texttt{Functional Scheme} @@ -4284,9 +4284,10 @@ right to left. \label{inversion}} \subsection{\tt functional inversion \ident} +\tacindex{functional inversion} \label{sec:functional-inversion} -\texttt{functional inversion} is a \emph{highly} experimental tactic +\texttt{functional inversion} is a tactic that performs inversion on hypothesis {\ident} of the form \texttt{\qualid\ \term$_1$\dots\term$_n$\ = \term} or \texttt{\term\ = \qualid\ \term$_1$\dots\term$_n$} where \qualid\ must have been |