1.1 --- a/doc-src/Ref/tctical.tex Thu May 11 10:33:07 1995 +0200
1.2 +++ b/doc-src/Ref/tctical.tex Thu May 11 10:38:30 1995 +0200
1.3 @@ -169,7 +169,7 @@
1.4 CHANGED : tactic -> tactic
1.5 \end{ttbox}
1.6 \begin{ttdescription}
1.7 -\item[\tt FILTER {\it p} $tac$]
1.8 +\item[\ttindexbold{FILTER} {\it p} $tac$]
1.9 applies $tac$ to the proof state and returns a sequence consisting of those
1.10 result states that satisfy~$p$.
1.11
1.12 @@ -258,7 +258,7 @@
1.13 DETERM : tactic -> tactic
1.14 \end{ttbox}
1.15 \begin{ttdescription}
1.16 -\item[COND {\it p} $tac@1$ $tac@2$]
1.17 +\item[\ttindexbold{COND} {\it p} $tac@1$ $tac@2$]
1.18 applies $tac@1$ to the proof state if it satisfies~$p$, and applies $tac@2$
1.19 otherwise. It is a conditional tactical in that only one of $tac@1$ and
1.20 $tac@2$ is applied to a proof state. However, both $tac@1$ and $tac@2$ are