doc-src/Ref/tctical.tex
changeset 1118 93ba05d8ccdc
parent 332 01b87a921967
child 3108 335efc3f5632
     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