diff options
author | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-03-04 12:10:31 +0100 |
---|---|---|
committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-03-05 14:14:25 +0100 |
commit | ba0a37d773c5d42f96b3b88714767ba2e7fb7a3b (patch) | |
tree | 5d849636ca0b37d9169c5d4e32610b369439470b /doc | |
parent | 39ec5b14518c35450aa0d9be2ab1012f5bd2f8e3 (diff) |
Deprecate Focus and Unfocus.
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 0113c8df3..bd74a40d7 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. |