equal
deleted
inserted
replaced
124 \ttindexbold{TRY} and \ttindexbold{REPEAT} (ignoring tracing) can be coded |
124 \ttindexbold{TRY} and \ttindexbold{REPEAT} (ignoring tracing) can be coded |
125 as follows: |
125 as follows: |
126 \begin{ttbox} |
126 \begin{ttbox} |
127 fun TRY tac = tac ORELSE all_tac; |
127 fun TRY tac = tac ORELSE all_tac; |
128 |
128 |
129 fun REPEAT tac = Tactic |
129 fun REPEAT tac = |
130 (fn state => tapply((tac THEN REPEAT tac) ORELSE all_tac, |
130 (fn state => ((tac THEN REPEAT tac) ORELSE all_tac) state); |
131 state)); |
|
132 \end{ttbox} |
131 \end{ttbox} |
133 If $tac$ can return multiple outcomes then so can \hbox{\tt REPEAT $tac$}. |
132 If $tac$ can return multiple outcomes then so can \hbox{\tt REPEAT $tac$}. |
134 Since {\tt REPEAT} uses \ttindex{ORELSE} and not {\tt APPEND} or {\tt |
133 Since {\tt REPEAT} uses \ttindex{ORELSE} and not {\tt APPEND} or {\tt |
135 INTLEAVE}, it applies $tac$ as many times as possible in each |
134 INTLEAVE}, it applies $tac$ as many times as possible in each |
136 outcome. |
135 outcome. |