diff options
| -rw-r--r-- | doc/refman/RefMan-pro.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index eeeb983df0..d69098d0b5 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -259,7 +259,7 @@ there is no focused goal left). Unfocusing is then handled by {\tt \}} Alternatively to {\tt \{} and {\tt \}}, proofs can be structured with bullets. The use of a bullet $b$ for the first time focuses on the first goal $g$, the same bullet cannot be used again until the proof -of $g$ is completed, then it is mandatory to focus the bext goal with $b$. The +of $g$ is completed, then it is mandatory to focus the next goal with $b$. The consequence is that $g$ and all goals present when $g$ was focused are focused with the same bullet $b$. See the example below. |