diff options
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 |