diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-pro.tex | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 0113c8df34..bd74a40d7c 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -298,13 +298,17 @@ subgoals which clutter your screen. \begin{Variant} \item {\tt Focus {\num}.}\\ This focuses the attention on the $\num^{th}$ subgoal to prove. - \end{Variant} +\emph{This command is deprecated since 8.8: prefer the use of bullets or + focusing brackets instead, including {\tt {\num}: \{}}. + \subsection[\tt Unfocus.]{\tt Unfocus.\comindex{Unfocus}} This command restores to focus the goal that were suspended by the last {\tt Focus} command. +\emph{This command is deprecated since 8.8.} + \subsection[\tt Unfocused.]{\tt Unfocused.\comindex{Unfocused}} Succeeds in the proof if fully unfocused, fails if there are some goals out of focus. |