# HG changeset patch
# User lcp
# Date 800181510 -7200
# Node ID 93ba05d8ccdceb813e479a9aa839af1d9667ddea
# Parent  839ab9c054f67b534eefb736322e7429938efc42
Indexing of FILTER and COND

diff -r 839ab9c054f6 -r 93ba05d8ccdc doc-src/Ref/tctical.tex
--- a/doc-src/Ref/tctical.tex	Thu May 11 10:33:07 1995 +0200
+++ b/doc-src/Ref/tctical.tex	Thu May 11 10:38:30 1995 +0200
@@ -169,7 +169,7 @@
 CHANGED : tactic -> tactic
 \end{ttbox}
 \begin{ttdescription}
-\item[\tt FILTER {\it p} $tac$] 
+\item[\ttindexbold{FILTER} {\it p} $tac$] 
 applies $tac$ to the proof state and returns a sequence consisting of those
 result states that satisfy~$p$.
 
@@ -258,7 +258,7 @@
 DETERM      : tactic -> tactic
 \end{ttbox}
 \begin{ttdescription}
-\item[COND {\it p} $tac@1$ $tac@2$] 
+\item[\ttindexbold{COND} {\it p} $tac@1$ $tac@2$] 
 applies $tac@1$ to the proof state if it satisfies~$p$, and applies $tac@2$
 otherwise.  It is a conditional tactical in that only one of $tac@1$ and
 $tac@2$ is applied to a proof state.  However, both $tac@1$ and $tac@2$ are