author lcp Thu, 11 May 1995 10:38:30 +0200 changeset 1118 93ba05d8ccdc parent 1117 839ab9c054f6 child 1119 49ed9a415637
Indexing of FILTER and COND
 doc-src/Ref/tctical.tex file | annotate | diff | comparison | revisions
--- 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