--- a/doc-src/IsarImplementation/Thy/Tactic.thy Wed Jan 25 21:14:00 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/Tactic.thy Wed Jan 25 22:01:15 2012 +0100
@@ -586,4 +586,66 @@
fun REPEAT tac = (tac THEN REPEAT tac) ORELSE all_tac;
*}
+
+subsection {* Scanning for a subgoal by number *}
+
+text {* Tactics with explicit subgoal addressing
+ @{ML_type "int -> tactic"} can be used together with tacticals that
+ act like ``subgoal quantifiers'': guided by success of the body
+ tactic a certain range of subgoals is covered. Thus the body tactic
+ is applied to all subgoals, for example.
+
+ Suppose that the goal state has @{text "n \<ge> 0"} subgoals. Many of
+ these tacticals address subgoal ranges counting downwards from
+ @{text "n"} towards @{text "1"}. This has the fortunate effect that
+ newly emerging subgoals are concatenated in the result, without
+ interfering each other. Nonetheless, there might be situations
+ where a different order is desired, but it has to be achieved by
+ other means. *}
+
+text %mlref {*
+ \begin{mldecls}
+ @{index_ML ALLGOALS: "(int -> tactic) -> tactic"} \\
+ @{index_ML TRYALL: "(int -> tactic) -> tactic"} \\
+ @{index_ML SOMEGOAL: "(int -> tactic) -> tactic"} \\
+ @{index_ML FIRSTGOAL: "(int -> tactic) -> tactic"} \\
+ @{index_ML REPEAT_SOME: "(int -> tactic) -> tactic"} \\
+ @{index_ML REPEAT_FIRST: "(int -> tactic) -> tactic"} \\
+ @{index_ML trace_goalno_tac: "(int -> tactic) -> int -> tactic"} \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item @{ML ALLGOALS}~@{text "tac"} is equivalent to @{text "tac
+ n"}~@{ML_op THEN}~@{text "\<dots>"}~@{ML_op THEN}~@{text "tac 1"}. It
+ applies the @{text tac} to all the subgoals, counting downwards.
+
+ \item @{ML TRYALL}~@{text "tac"} is equivalent to @{ML TRY}~@{text
+ "(tac n)"}~@{ML_op THEN}~@{text "\<dots>"}~@{ML_op THEN}~@{ML TRY}~@{text
+ "(tac 1)"}. It attempts to apply @{text "tac"} to all the subgoals.
+
+ \item @{ML SOMEGOAL}~@{text "tac"} is equivalent to @{text "tac
+ n"}~@{ML_op ORELSE}~@{text "\<dots>"}~@{ML_op ORELSE}~@{text "tac 1"}. It
+ applies @{text "tac"} to one subgoal, counting downwards.
+
+ \item @{ML FIRSTGOAL}~@{text "tac"} is equivalent to @{text "tac
+ 1"}~@{ML_op ORELSE}~@{text "\<dots>"}~@{ML_op ORELSE}~@{text "tac n"}. It
+ applies @{text "tac"} to one subgoal, counting upwards.
+
+ \item @{ML REPEAT_SOME}~@{text "tac"} applies @{text "tac"} once or
+ more to a subgoal, counting downwards.
+
+ \item @{ML REPEAT_FIRST}~@{text "tac"} applies @{text "tac"} once or
+ more to a subgoal, counting upwards.
+
+ \item @{ML trace_goalno_tac}~@{text "tac i"} applies @{text "tac i"}
+ to the proof state. If the resulting sequence is non-empty, then it
+ is returned, with the side-effect of printing the selected subgoal.
+ Otherwise, it fails and prints nothing. It indicates that ``the
+ tactic worked for subgoal @{text "i"}'' and is mainly used with @{ML
+ SOMEGOAL} and @{ML FIRSTGOAL}.
+
+ \end{description}
+*}
+
end
--- a/doc-src/IsarImplementation/Thy/document/Tactic.tex Wed Jan 25 21:14:00 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex Wed Jan 25 22:01:15 2012 +0100
@@ -728,10 +728,82 @@
\isadelimML
%
\endisadelimML
-\isanewline
+%
+\isamarkupsubsection{Scanning for a subgoal by number%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Tactics with explicit subgoal addressing
+ \verb|int -> tactic| can be used together with tacticals that
+ act like ``subgoal quantifiers'': guided by success of the body
+ tactic a certain range of subgoals is covered. Thus the body tactic
+ is applied to all subgoals, for example.
+
+ Suppose that the goal state has \isa{n\ {\isaliteral{5C3C67653E}{\isasymge}}\ {\isadigit{0}}} subgoals. Many of
+ these tacticals address subgoal ranges counting downwards from
+ \isa{n} towards \isa{{\isadigit{1}}}. This has the fortunate effect that
+ newly emerging subgoals are concatenated in the result, without
+ interfering each other. Nonetheless, there might be situations
+ where a different order is desired, but it has to be achieved by
+ other means.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexdef{}{ML}{ALLGOALS}\verb|ALLGOALS: (int -> tactic) -> tactic| \\
+ \indexdef{}{ML}{TRYALL}\verb|TRYALL: (int -> tactic) -> tactic| \\
+ \indexdef{}{ML}{SOMEGOAL}\verb|SOMEGOAL: (int -> tactic) -> tactic| \\
+ \indexdef{}{ML}{FIRSTGOAL}\verb|FIRSTGOAL: (int -> tactic) -> tactic| \\
+ \indexdef{}{ML}{REPEAT\_SOME}\verb|REPEAT_SOME: (int -> tactic) -> tactic| \\
+ \indexdef{}{ML}{REPEAT\_FIRST}\verb|REPEAT_FIRST: (int -> tactic) -> tactic| \\
+ \indexdef{}{ML}{trace\_goalno\_tac}\verb|trace_goalno_tac: (int -> tactic) -> int -> tactic| \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item \verb|ALLGOALS|~\isa{tac} is equivalent to \isa{tac\ n}~\verb|THEN|~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb|THEN|~\isa{tac\ {\isadigit{1}}}. It
+ applies the \isa{tac} to all the subgoals, counting downwards.
+
+ \item \verb|TRYALL|~\isa{tac} is equivalent to \verb|TRY|~\isa{{\isaliteral{28}{\isacharparenleft}}tac\ n{\isaliteral{29}{\isacharparenright}}}~\verb|THEN|~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb|THEN|~\verb|TRY|~\isa{{\isaliteral{28}{\isacharparenleft}}tac\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}}. It attempts to apply \isa{tac} to all the subgoals.
+
+ \item \verb|SOMEGOAL|~\isa{tac} is equivalent to \isa{tac\ n}~\verb|ORELSE|~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb|ORELSE|~\isa{tac\ {\isadigit{1}}}. It
+ applies \isa{tac} to one subgoal, counting downwards.
+
+ \item \verb|FIRSTGOAL|~\isa{tac} is equivalent to \isa{tac\ {\isadigit{1}}}~\verb|ORELSE|~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb|ORELSE|~\isa{tac\ n}. It
+ applies \isa{tac} to one subgoal, counting upwards.
+
+ \item \verb|REPEAT_SOME|~\isa{tac} applies \isa{tac} once or
+ more to a subgoal, counting downwards.
+
+ \item \verb|REPEAT_FIRST|~\isa{tac} applies \isa{tac} once or
+ more to a subgoal, counting upwards.
+
+ \item \verb|trace_goalno_tac|~\isa{tac\ i} applies \isa{tac\ i}
+ to the proof state. If the resulting sequence is non-empty, then it
+ is returned, with the side-effect of printing the selected subgoal.
+ Otherwise, it fails and prints nothing. It indicates that ``the
+ tactic worked for subgoal \isa{i}'' and is mainly used with \verb|SOMEGOAL| and \verb|FIRSTGOAL|.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
%
\isadelimtheory
-\isanewline
%
\endisadelimtheory
%
--- a/doc-src/Ref/tctical.tex Wed Jan 25 21:14:00 2012 +0100
+++ b/doc-src/Ref/tctical.tex Wed Jan 25 22:01:15 2012 +0100
@@ -204,71 +204,6 @@
\end{ttdescription}
-
-\subsection{Scanning for a subgoal by number}
-\index{tacticals!scanning for subgoals}
-\begin{ttbox}
-ALLGOALS : (int -> tactic) -> tactic
-TRYALL : (int -> tactic) -> tactic
-SOMEGOAL : (int -> tactic) -> tactic
-FIRSTGOAL : (int -> tactic) -> tactic
-REPEAT_SOME : (int -> tactic) -> tactic
-REPEAT_FIRST : (int -> tactic) -> tactic
-trace_goalno_tac : (int -> tactic) -> int -> tactic
-\end{ttbox}
-These apply a tactic function of type {\tt int -> tactic} to all the
-subgoal numbers of a proof state, and join the resulting tactics using
-\ttindex{THEN} or \ttindex{ORELSE}\@. Thus, they apply the tactic to all the
-subgoals, or to one subgoal.
-
-Suppose that the original proof state has $n$ subgoals.
-
-\begin{ttdescription}
-\item[\ttindexbold{ALLGOALS} {\it tacf}]
-is equivalent to
-\hbox{\tt$tacf(n)$ THEN \ldots{} THEN $tacf(1)$}.
-
-It applies {\it tacf} to all the subgoals, counting downwards (to
-avoid problems when subgoals are added or deleted).
-
-\item[\ttindexbold{TRYALL} {\it tacf}]
-is equivalent to
-\hbox{\tt TRY$(tacf(n))$ THEN \ldots{} THEN TRY$(tacf(1))$}.
-
-It attempts to apply {\it tacf} to all the subgoals. For instance,
-the tactic \hbox{\tt TRYALL assume_tac} attempts to solve all the subgoals by
-assumption.
-
-\item[\ttindexbold{SOMEGOAL} {\it tacf}]
-is equivalent to
-\hbox{\tt$tacf(n)$ ORELSE \ldots{} ORELSE $tacf(1)$}.
-
-It applies {\it tacf} to one subgoal, counting downwards. For instance,
-the tactic \hbox{\tt SOMEGOAL assume_tac} solves one subgoal by assumption,
-failing if this is impossible.
-
-\item[\ttindexbold{FIRSTGOAL} {\it tacf}]
-is equivalent to
-\hbox{\tt$tacf(1)$ ORELSE \ldots{} ORELSE $tacf(n)$}.
-
-It applies {\it tacf} to one subgoal, counting upwards.
-
-\item[\ttindexbold{REPEAT_SOME} {\it tacf}]
-applies {\it tacf} once or more to a subgoal, counting downwards.
-
-\item[\ttindexbold{REPEAT_FIRST} {\it tacf}]
-applies {\it tacf} once or more to a subgoal, counting upwards.
-
-\item[\ttindexbold{trace_goalno_tac} {\it tac} {\it i}]
-applies \hbox{\it tac i\/} to the proof state. If the resulting sequence
-is non-empty, then it is returned, with the side-effect of printing {\tt
-Subgoal~$i$ selected}. Otherwise, {\tt trace_goalno_tac} returns the empty
-sequence and prints nothing.
-
-It indicates that `the tactic worked for subgoal~$i$' and is mainly used
-with {\tt SOMEGOAL} and {\tt FIRSTGOAL}.
-\end{ttdescription}
-
\index{tacticals|)}