diff options
| author | Maxime Dénès | 2017-08-18 15:49:42 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-08-18 15:49:42 +0200 |
| commit | 7221e3644b2503a8ba5e3c94eb703bd2bf0967b4 (patch) | |
| tree | 1943cf7849f4eb293dc76a4502e5b9911053b1f4 /doc/refman/RefMan-pro.tex | |
| parent | 26f71fb401ceb3e157a34b27102fa0d1e586f383 (diff) | |
| parent | 7ca4cd26d67070058589031b693454cd2858e4e9 (diff) | |
Merge PR #973: 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 95fee3241c..eb59ca584e 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 |