--- a/doc-src/IsarImplementation/Thy/Tactic.thy Wed Jan 25 16:16:20 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/Tactic.thy Wed Jan 25 18:18:59 2012 +0100
@@ -399,15 +399,88 @@
section {* Tacticals \label{sec:tacticals} *}
-text {*
- A \emph{tactical} is a functional combinator for building up complex
- tactics from simpler ones. Typical tactical perform sequential
- composition, disjunction (choice), iteration, or goal addressing.
- Various search strategies may be expressed via tacticals.
+text {* A \emph{tactical} is a functional combinator for building up
+ complex tactics from simpler ones. Common tacticals perform
+ sequential composition, disjunctive choice, iteration, or goal
+ addressing. Various search strategies may be expressed via
+ tacticals.
+
+ \medskip The chapter on tacticals in old \cite{isabelle-ref} is
+ still applicable for further details. *}
+
+
+subsection {* Combining tactics *}
+
+text {* Sequential composition and alternative choices are the most
+ basic ways to combine tactics, similarly to ``@{verbatim ","}'' and
+ ``@{verbatim "|"}'' in Isar method notation. This corresponds to
+ @{text "THEN"} and @{text "ORELSE"} in ML, but there are further
+ possibilities for fine-tuning alternation of tactics such as @{text
+ "APPEND"}. Further details become visible in ML due to explicit
+ subgoal addressing. *}
+
+text %mlref {*
+ \begin{mldecls}
+ @{index_ML "op THEN": "tactic * tactic -> tactic"} \\
+ @{index_ML "op ORELSE": "tactic * tactic -> tactic"} \\
+ @{index_ML "op APPEND": "tactic * tactic -> tactic"} \\
+ @{index_ML "EVERY": "tactic list -> tactic"} \\
+ @{index_ML "FIRST": "tactic list -> tactic"} \\[0.5ex]
+
+ @{index_ML "op THEN'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
+ @{index_ML "op ORELSE'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
+ @{index_ML "op APPEND'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
+ @{index_ML "EVERY'": "('a -> tactic) list -> 'a -> tactic"} \\
+ @{index_ML "FIRST'": "('a -> tactic) list -> 'a -> tactic"} \\
+ @{index_ML "EVERY1": "(int -> tactic) list -> tactic"} \\
+ @{index_ML "FIRST1": "(int -> tactic) list -> tactic"} \\[0.5ex]
+ \end{mldecls}
+
+ \begin{description}
- \medskip FIXME
+ \item @{text "tac\<^sub>1 THEN tac\<^sub>2"} is the sequential composition of
+ @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Applied to a proof state, it
+ returns all states reachable in two steps by applying @{text "tac\<^sub>1"}
+ followed by @{text "tac\<^sub>2"}. First, it applies @{text "tac\<^sub>1"} to the
+ proof state, getting a sequence of possible next states; then, it
+ applies @{text "tac\<^sub>2"} to each of these and concatenates the results
+ to produce again one flat sequence of states.
+
+ \item @{text "tac\<^sub>1 ORELSE tac\<^sub>2"} makes a choice between @{text
+ "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Applied to a state, it tries @{text
+ "tac\<^sub>1"} and returns the result if non-empty; if @{text "tac\<^sub>1"} fails
+ then it uses @{text "tac\<^sub>2"}. This is a deterministic choice: if
+ @{text "tac\<^sub>1"} succeeds then @{text "tac\<^sub>2"} is excluded from the
+ result.
+
+ \item @{text "tac\<^sub>1 APPEND tac\<^sub>2"} concatenates the possible results
+ of @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Unlike @{text "ORELSE"} there
+ is \emph{no commitment} to either tactic, so @{text "APPEND"} helps
+ to avoid incompleteness during search, at the cost of potential
+ inefficiencies.
- \medskip The chapter on tacticals in \cite{isabelle-ref} is still
- applicable, despite a few outdated details. *}
+ \item @{text "EVERY [tac\<^sub>1, \<dots>, tac\<^sub>n]"} abbreviates @{text "tac\<^sub>1 THEN
+ \<dots> THEN tac\<^sub>n"}. Note that @{text "EVERY []"} is the same as @{ML
+ all_tac}: it always succeeds.
+
+ \item @{text "FIRST [tac\<^sub>1, \<dots>, tac\<^sub>n]"} abbreviates @{text "tac\<^sub>1
+ ORELSE \<dots> ORELSE tac\<^sub>n"}. Note that @{text "FIRST []"} is the same as
+ @{ML no_tac}: it always fails.
+
+ \item @{text "THEN'"}, @{text "ORELSE'"}, and @{text "APPEND'"} are
+ lifted versions of @{text "THEN"}, @{text "ORELSE"}, and @{text
+ "APPEND"}, for tactics with explicit subgoal addressing. This means
+ @{text "(tac\<^sub>1 THEN' tac\<^sub>2) i"} is the same as @{text "(tac\<^sub>1 i THEN
+ tac\<^sub>2 i)"} etc.
+
+ \item @{text "EVERY'"} and @{text "FIRST'"} are lifted versions of
+ @{text "EVERY'"} and @{text "FIRST'"}, for tactics with explicit
+ subgoal addressing.
+
+ \item @{text "EVERY1"} and @{text "FIRST1"} are convenience versions
+ of @{text "EVERY'"} and @{text "FIRST'"}, applied to subgoal 1.
+
+ \end{description}
+*}
end
--- a/doc-src/IsarImplementation/Thy/document/Tactic.tex Wed Jan 25 16:16:20 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex Wed Jan 25 18:18:59 2012 +0100
@@ -476,18 +476,102 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-A \emph{tactical} is a functional combinator for building up complex
- tactics from simpler ones. Typical tactical perform sequential
- composition, disjunction (choice), iteration, or goal addressing.
- Various search strategies may be expressed via tacticals.
+A \emph{tactical} is a functional combinator for building up
+ complex tactics from simpler ones. Common tacticals perform
+ sequential composition, disjunctive choice, iteration, or goal
+ addressing. Various search strategies may be expressed via
+ tacticals.
- \medskip FIXME
-
- \medskip The chapter on tacticals in \cite{isabelle-ref} is still
- applicable, despite a few outdated details.%
+ \medskip The chapter on tacticals in old \cite{isabelle-ref} is
+ still applicable for further details.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Combining tactics%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Sequential composition and alternative choices are the most
+ basic ways to combine tactics, similarly to ``\verb|,|'' and
+ ``\verb||\verb,|,\verb||'' in Isar method notation. This corresponds to
+ \isa{THEN} and \isa{ORELSE} in ML, but there are further
+ possibilities for fine-tuning alternation of tactics such as \isa{APPEND}. Further details become visible in ML due to explicit
+ subgoal addressing.%
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexdef{}{ML}{THEN}\verb|op THEN: tactic * tactic -> tactic| \\
+ \indexdef{}{ML}{ORELSE}\verb|op ORELSE: tactic * tactic -> tactic| \\
+ \indexdef{}{ML}{APPEND}\verb|op APPEND: tactic * tactic -> tactic| \\
+ \indexdef{}{ML}{EVERY}\verb|EVERY: tactic list -> tactic| \\
+ \indexdef{}{ML}{FIRST}\verb|FIRST: tactic list -> tactic| \\[0.5ex]
+
+ \indexdef{}{ML}{THEN'}\verb|op THEN': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic| \\
+ \indexdef{}{ML}{ORELSE'}\verb|op ORELSE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic| \\
+ \indexdef{}{ML}{APPEND'}\verb|op APPEND': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic| \\
+ \indexdef{}{ML}{EVERY'}\verb|EVERY': ('a -> tactic) list -> 'a -> tactic| \\
+ \indexdef{}{ML}{FIRST'}\verb|FIRST': ('a -> tactic) list -> 'a -> tactic| \\
+ \indexdef{}{ML}{EVERY1}\verb|EVERY1: (int -> tactic) list -> tactic| \\
+ \indexdef{}{ML}{FIRST1}\verb|FIRST1: (int -> tactic) list -> tactic| \\[0.5ex]
+ \end{mldecls}
+
+ \begin{description}
+
+ \item \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ THEN\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} is the sequential composition of
+ \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. Applied to a proof state, it
+ returns all states reachable in two steps by applying \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}
+ followed by \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. First, it applies \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} to the
+ proof state, getting a sequence of possible next states; then, it
+ applies \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} to each of these and concatenates the results
+ to produce again one flat sequence of states.
+
+ \item \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ ORELSE\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} makes a choice between \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. Applied to a state, it tries \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and returns the result if non-empty; if \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} fails
+ then it uses \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. This is a deterministic choice: if
+ \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} succeeds then \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} is excluded from the
+ result.
+
+ \item \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ APPEND\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} concatenates the possible results
+ of \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. Unlike \isa{ORELSE} there
+ is \emph{no commitment} to either tactic, so \isa{APPEND} helps
+ to avoid incompleteness during search, at the cost of potential
+ inefficiencies.
+
+ \item \isa{EVERY\ {\isaliteral{5B}{\isacharbrackleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5D}{\isacharbrackright}}} abbreviates \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ THEN\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ THEN\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n}. Note that \isa{EVERY\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} is the same as \verb|all_tac|: it always succeeds.
+
+ \item \isa{FIRST\ {\isaliteral{5B}{\isacharbrackleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5D}{\isacharbrackright}}} abbreviates \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ ORELSE\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ ORELSE\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n}. Note that \isa{FIRST\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} is the same as
+ \verb|no_tac|: it always fails.
+
+ \item \isa{THEN{\isaliteral{27}{\isacharprime}}}, \isa{ORELSE{\isaliteral{27}{\isacharprime}}}, and \isa{APPEND{\isaliteral{27}{\isacharprime}}} are
+ lifted versions of \isa{THEN}, \isa{ORELSE}, and \isa{APPEND}, for tactics with explicit subgoal addressing. This means
+ \isa{{\isaliteral{28}{\isacharparenleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ THEN{\isaliteral{27}{\isacharprime}}\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ i} is the same as \isa{{\isaliteral{28}{\isacharparenleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ i\ THEN\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ i{\isaliteral{29}{\isacharparenright}}} etc.
+
+ \item \isa{EVERY{\isaliteral{27}{\isacharprime}}} and \isa{FIRST{\isaliteral{27}{\isacharprime}}} are lifted versions of
+ \isa{EVERY{\isaliteral{27}{\isacharprime}}} and \isa{FIRST{\isaliteral{27}{\isacharprime}}}, for tactics with explicit
+ subgoal addressing.
+
+ \item \isa{EVERY{\isadigit{1}}} and \isa{FIRST{\isadigit{1}}} are convenience versions
+ of \isa{EVERY{\isaliteral{27}{\isacharprime}}} and \isa{FIRST{\isaliteral{27}{\isacharprime}}}, applied to subgoal 1.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
\isadelimtheory
%
\endisadelimtheory
--- a/doc-src/Ref/tctical.tex Wed Jan 25 16:16:20 2012 +0100
+++ b/doc-src/Ref/tctical.tex Wed Jan 25 18:18:59 2012 +0100
@@ -1,68 +1,7 @@
\chapter{Tacticals}
-\index{tacticals|(}
-Tacticals are operations on tactics. Their implementation makes use of
-functional programming techniques, especially for sequences. Most of the
-time, you may forget about this and regard tacticals as high-level control
-structures.
\section{The basic tacticals}
-\subsection{Joining two tactics}
-\index{tacticals!joining two tactics}
-The tacticals {\tt THEN} and {\tt ORELSE}, which provide sequencing and
-alternation, underlie most of the other control structures in Isabelle.
-{\tt APPEND} and {\tt INTLEAVE} provide more sophisticated forms of
-alternation.
-\begin{ttbox}
-THEN : tactic * tactic -> tactic \hfill{\bf infix 1}
-ORELSE : tactic * tactic -> tactic \hfill{\bf infix}
-APPEND : tactic * tactic -> tactic \hfill{\bf infix}
-INTLEAVE : tactic * tactic -> tactic \hfill{\bf infix}
-\end{ttbox}
-\begin{ttdescription}
-\item[$tac@1$ \ttindexbold{THEN} $tac@2$]
-is the sequential composition of the two tactics. Applied to a proof
-state, it returns all states reachable in two steps by applying $tac@1$
-followed by~$tac@2$. First, it applies $tac@1$ to the proof state, getting a
-sequence of next states; then, it applies $tac@2$ to each of these and
-concatenates the results.
-
-\item[$tac@1$ \ttindexbold{ORELSE} $tac@2$]
-makes a choice between the two tactics. Applied to a state, it
-tries~$tac@1$ and returns the result if non-empty; if $tac@1$ fails then it
-uses~$tac@2$. This is a deterministic choice: if $tac@1$ succeeds then
-$tac@2$ is excluded.
-
-\item[$tac@1$ \ttindexbold{APPEND} $tac@2$]
-concatenates the results of $tac@1$ and~$tac@2$. By not making a commitment
-to either tactic, {\tt APPEND} helps avoid incompleteness during
-search.\index{search}
-
-\item[$tac@1$ \ttindexbold{INTLEAVE} $tac@2$]
-interleaves the results of $tac@1$ and~$tac@2$. Thus, it includes all
-possible next states, even if one of the tactics returns an infinite
-sequence.
-\end{ttdescription}
-
-
-\subsection{Joining a list of tactics}
-\index{tacticals!joining a list of tactics}
-\begin{ttbox}
-EVERY : tactic list -> tactic
-FIRST : tactic list -> tactic
-\end{ttbox}
-{\tt EVERY} and {\tt FIRST} are block structured versions of {\tt THEN} and
-{\tt ORELSE}\@.
-\begin{ttdescription}
-\item[\ttindexbold{EVERY} {$[tac@1,\ldots,tac@n]$}]
-abbreviates \hbox{\tt$tac@1$ THEN \ldots{} THEN $tac@n$}. It is useful for
-writing a series of tactics to be executed in sequence.
-
-\item[\ttindexbold{FIRST} {$[tac@1,\ldots,tac@n]$}]
-abbreviates \hbox{\tt$tac@1$ ORELSE \ldots{} ORELSE $tac@n$}. It is useful for
-writing a series of tactics to be attempted one after another.
-\end{ttdescription}
-
\subsection{Repetition tacticals}
\index{tacticals!repetition}
@@ -128,8 +67,10 @@
\item[\ttindexbold{no_tac}]
maps any proof state to the empty sequence. Thus it succeeds for no state.
-It is the identity element of \ttindex{ORELSE}, \ttindex{APPEND}, and
-\ttindex{INTLEAVE}\@. Also, it is a zero element for \ttindex{THEN}, which means that
+It is the identity element of \ttindex{ORELSE}, and
+\ttindex{APPEND}\@. Also, it is a zero element for \ttindex{THEN},
+which means that
+
\hbox{\tt$tac$ THEN no_tac} is equivalent to {\tt no_tac}.
\end{ttdescription}
These primitive tactics are useful when writing tacticals. For example,
@@ -142,9 +83,8 @@
(fn state => ((tac THEN REPEAT tac) ORELSE all_tac) state);
\end{ttbox}
If $tac$ can return multiple outcomes then so can \hbox{\tt REPEAT $tac$}.
-Since {\tt REPEAT} uses \ttindex{ORELSE} and not {\tt APPEND} or {\tt
-INTLEAVE}, it applies $tac$ as many times as possible in each
-outcome.
+Since {\tt REPEAT} uses \ttindex{ORELSE} and not {\tt APPEND}, it
+applies $tac$ as many times as possible in each outcome.
\begin{warn}
Note {\tt REPEAT}'s explicit abstraction over the proof state. Recursive
@@ -429,79 +369,6 @@
with {\tt SOMEGOAL} and {\tt FIRSTGOAL}.
\end{ttdescription}
-
-\subsection{Joining tactic functions}
-\index{tacticals!joining tactic functions}
-\begin{ttbox}
-THEN' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic \hfill{\bf infix 1}
-ORELSE' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic \hfill{\bf infix}
-APPEND' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic \hfill{\bf infix}
-INTLEAVE' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic \hfill{\bf infix}
-EVERY' : ('a -> tactic) list -> 'a -> tactic
-FIRST' : ('a -> tactic) list -> 'a -> tactic
-\end{ttbox}
-These help to express tactics that specify subgoal numbers. The tactic
-\begin{ttbox}
-SOMEGOAL (fn i => resolve_tac rls i ORELSE eresolve_tac erls i)
-\end{ttbox}
-can be simplified to
-\begin{ttbox}
-SOMEGOAL (resolve_tac rls ORELSE' eresolve_tac erls)
-\end{ttbox}
-Note that {\tt TRY'}, {\tt REPEAT'}, {\tt DEPTH_FIRST'}, etc.\ are not
-provided, because function composition accomplishes the same purpose.
-The tactic
-\begin{ttbox}
-ALLGOALS (fn i => REPEAT (etac exE i ORELSE atac i))
-\end{ttbox}
-can be simplified to
-\begin{ttbox}
-ALLGOALS (REPEAT o (etac exE ORELSE' atac))
-\end{ttbox}
-These tacticals are polymorphic; $x$ need not be an integer.
-\begin{center} \tt
-\begin{tabular}{r@{\rm\ \ yields\ \ }l}
- $(tacf@1$~~THEN'~~$tacf@2)(x)$ \index{*THEN'} &
- $tacf@1(x)$~~THEN~~$tacf@2(x)$ \\
-
- $(tacf@1$ ORELSE' $tacf@2)(x)$ \index{*ORELSE'} &
- $tacf@1(x)$ ORELSE $tacf@2(x)$ \\
-
- $(tacf@1$ APPEND' $tacf@2)(x)$ \index{*APPEND'} &
- $tacf@1(x)$ APPEND $tacf@2(x)$ \\
-
- $(tacf@1$ INTLEAVE' $tacf@2)(x)$ \index{*INTLEAVE'} &
- $tacf@1(x)$ INTLEAVE $tacf@2(x)$ \\
-
- EVERY' $[tacf@1,\ldots,tacf@n] \; (x)$ \index{*EVERY'} &
- EVERY $[tacf@1(x),\ldots,tacf@n(x)]$ \\
-
- FIRST' $[tacf@1,\ldots,tacf@n] \; (x)$ \index{*FIRST'} &
- FIRST $[tacf@1(x),\ldots,tacf@n(x)]$
-\end{tabular}
-\end{center}
-
-
-\subsection{Applying a list of tactics to 1}
-\index{tacticals!joining tactic functions}
-\begin{ttbox}
-EVERY1: (int -> tactic) list -> tactic
-FIRST1: (int -> tactic) list -> tactic
-\end{ttbox}
-A common proof style is to treat the subgoals as a stack, always
-restricting attention to the first subgoal. Such proofs contain long lists
-of tactics, each applied to~1. These can be simplified using {\tt EVERY1}
-and {\tt FIRST1}:
-\begin{center} \tt
-\begin{tabular}{r@{\rm\ \ abbreviates\ \ }l}
- EVERY1 $[tacf@1,\ldots,tacf@n]$ \indexbold{*EVERY1} &
- EVERY $[tacf@1(1),\ldots,tacf@n(1)]$ \\
-
- FIRST1 $[tacf@1,\ldots,tacf@n]$ \indexbold{*FIRST1} &
- FIRST $[tacf@1(1),\ldots,tacf@n(1)]$
-\end{tabular}
-\end{center}
-
\index{tacticals|)}