diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-08-16 16:32:44 +0200 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-08-17 10:42:03 +0200 |
| commit | 7ca4cd26d67070058589031b693454cd2858e4e9 (patch) | |
| tree | 495fbbdac5c9cfe688ca4bc7edc1b293dac189a2 /doc/refman/RefMan-pro.tex | |
| parent | 16b0b833a3cee070a207e2039bde0ae77b8774d4 (diff) | |
Adding documentation for Printing Focused option.
Diffstat (limited to 'doc/refman/RefMan-pro.tex')
| -rw-r--r-- | doc/refman/RefMan-pro.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 95fee3241..eb59ca584 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -308,7 +308,7 @@ last {\tt Focus} command. Succeeds in the proof is fully unfocused, fails is there are some goals out of focus. -\subsection[\tt \{ \textrm{and} \}]{\tt \{ \textrm{and} \}\comindex{\{}\comindex{\}}} +\subsection[\tt \{ \textrm{and} \}]{\tt \{ \textrm{and} \}\comindex{\{}\comindex{\}}}\label{curlybacket} The command {\tt \{} (without a terminating period) focuses on the first goal, much like {\tt Focus.} does, however, the subproof can only be unfocused when it has been fully solved (\emph{i.e.} when @@ -327,7 +327,7 @@ unfocus it or focus the next one. \end{ErrMsgs} \subsection[Bullets]{Bullets\comindex{+ (command)} - \comindex{- (command)}\comindex{* (command)}\index{Bullets}} + \comindex{- (command)}\comindex{* (command)}\index{Bullets}}\label{bullets} 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 |