doc-src/Ref/tctical.tex
changeset 1118 93ba05d8ccdc
parent 332 01b87a921967
child 3108 335efc3f5632
equal deleted inserted replaced
1117:839ab9c054f6 1118:93ba05d8ccdc
   167 \begin{ttbox} 
   167 \begin{ttbox} 
   168 FILTER  : (thm -> bool) -> tactic -> tactic
   168 FILTER  : (thm -> bool) -> tactic -> tactic
   169 CHANGED : tactic -> tactic
   169 CHANGED : tactic -> tactic
   170 \end{ttbox}
   170 \end{ttbox}
   171 \begin{ttdescription}
   171 \begin{ttdescription}
   172 \item[\tt FILTER {\it p} $tac$] 
   172 \item[\ttindexbold{FILTER} {\it p} $tac$] 
   173 applies $tac$ to the proof state and returns a sequence consisting of those
   173 applies $tac$ to the proof state and returns a sequence consisting of those
   174 result states that satisfy~$p$.
   174 result states that satisfy~$p$.
   175 
   175 
   176 \item[\ttindexbold{CHANGED} {\it tac}] 
   176 \item[\ttindexbold{CHANGED} {\it tac}] 
   177 applies {\it tac\/} to the proof state and returns precisely those states
   177 applies {\it tac\/} to the proof state and returns precisely those states
   256 COND        : (thm->bool) -> tactic -> tactic -> tactic
   256 COND        : (thm->bool) -> tactic -> tactic -> tactic
   257 IF_UNSOLVED : tactic -> tactic
   257 IF_UNSOLVED : tactic -> tactic
   258 DETERM      : tactic -> tactic
   258 DETERM      : tactic -> tactic
   259 \end{ttbox}
   259 \end{ttbox}
   260 \begin{ttdescription}
   260 \begin{ttdescription}
   261 \item[COND {\it p} $tac@1$ $tac@2$] 
   261 \item[\ttindexbold{COND} {\it p} $tac@1$ $tac@2$] 
   262 applies $tac@1$ to the proof state if it satisfies~$p$, and applies $tac@2$
   262 applies $tac@1$ to the proof state if it satisfies~$p$, and applies $tac@2$
   263 otherwise.  It is a conditional tactical in that only one of $tac@1$ and
   263 otherwise.  It is a conditional tactical in that only one of $tac@1$ and
   264 $tac@2$ is applied to a proof state.  However, both $tac@1$ and $tac@2$ are
   264 $tac@2$ is applied to a proof state.  However, both $tac@1$ and $tac@2$ are
   265 evaluated because \ML{} uses eager evaluation.
   265 evaluated because \ML{} uses eager evaluation.
   266 
   266