diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 11:24:27 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 11:24:27 +0100 |
commit | c5432539927de8a94d5c549d288b95b7215390b9 (patch) | |
tree | a894769d27c70c780f684ff63b5e547556186a91 /doc | |
parent | 76058420ec0ea037504adf0af213d0542bd7c1c3 (diff) | |
parent | ba0a37d773c5d42f96b3b88714767ba2e7fb7a3b (diff) |
Merge PR #6909: Deprecate Focus and Unfocus
Diffstat (limited to 'doc')
-rw-r--r-- | doc/refman/RefMan-pro.tex | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 6b24fdde7..bd74a40d7 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -298,15 +298,19 @@ 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 is fully unfocused, fails is there are some +Succeeds in the proof if fully unfocused, fails if there are some goals out of focus. \subsection[\tt \{ \textrm{and} \}]{\tt \{ \textrm{and} \}\comindex{\{}\comindex{\}}}\label{curlybacket} |