updated repetition tacticals;
discontinued odd trace_REPEAT (assumes sequential TTY loop);

--- a/doc-src/IsarImplementation/Thy/Tactic.thy	Wed Jan 25 18:18:59 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/Tactic.thy	Wed Jan 25 19:04:38 2012 +0100
@@ -483,4 +483,111 @@
   \end{description}
 *}
 
+
+subsection {* Repetition tacticals *}
+
+text {* These tacticals provide further control over repetition of
+  tactics, beyond the stylized forms of ``@{verbatim "?"}''  and
+  ``@{verbatim "+"}'' in Isar method expressions. *}
+
+text %mlref {*
+  \begin{mldecls}
+  @{index_ML "TRY": "tactic -> tactic"} \\
+  @{index_ML "REPEAT_DETERM": "tactic -> tactic"} \\
+  @{index_ML "REPEAT_DETERM_N": "int -> tactic -> tactic"} \\
+  @{index_ML "REPEAT": "tactic -> tactic"} \\
+  @{index_ML "REPEAT1": "tactic -> tactic"} \\
+  @{index_ML "DETERM_UNTIL": "(thm -> bool) -> tactic -> tactic"} \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item @{ML TRY}~@{text "tac"} applies @{text "tac"} to the proof
+  state and returns the resulting sequence, if non-empty; otherwise it
+  returns the original state.  Thus, it applies @{text "tac"} at most
+  once.
+
+  \item @{ML REPEAT_DETERM}~@{text "tac"} applies @{text "tac"} to the
+  proof state and, recursively, to the head of the resulting sequence.
+  It returns the first state to make @{text "tac"} fail.  It is
+  deterministic, discarding alternative outcomes.
+
+  \item @{ML REPEAT_DETERM_N}~@{text "n tac"} is like @{ML
+  REPEAT_DETERM}~@{text "tac"} but the number of repetitions is bound
+  by @{text "n"} (where @{ML "~1"} means @{text "\<infinity>"}).
+
+  \item @{ML REPEAT}~@{text "tac"} applies @{text "tac"} to the proof
+  state and, recursively, to each element of the resulting sequence.
+  The resulting sequence consists of those states that make @{text
+  "tac"} fail.  Thus, it applies @{text "tac"} as many times as
+  possible (including zero times), and allows backtracking over each
+  invocation of @{text "tac"}.  @{ML REPEAT} is more general than @{ML
+  REPEAT_DETERM}, but requires more space.
+
+  \item @{ML REPEAT1}~@{text "tac"} is like @{ML REPEAT}~@{text "tac"}
+  but it always applies @{text "tac"} at least once, failing if this
+  is impossible.
+
+  \item @{ML DETERM_UNTIL}~@{text "P tac"} applies @{text "tac"} to
+  the proof state and, recursively, to the head of the resulting
+  sequence, until the predicate @{text "P"} (applied on the proof
+  state) yields @{ML true}. It fails if @{text "tac"} fails on any of
+  the intermediate states. It is deterministic, discarding alternative
+  outcomes.
+
+  \end{description}
+*}
+
+
+subsection {* Identities for tacticals *}
+
+text %mlref {*
+  \begin{mldecls}
+  @{index_ML all_tac: tactic} \\
+  @{index_ML no_tac: tactic} \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item @{ML all_tac} maps any proof state to the one-element sequence
+  containing that state.  Thus, it succeeds for all states.  It is the
+  identity element of the tactical @{ML "op THEN"}.
+
+  \item @{ML no_tac} maps any proof state to the empty sequence.  Thus
+  it succeeds for no state.  It is the identity element of
+  @{ML "op ORELSE"} and @{ML "op APPEND"}.  Also, it is a zero element
+  for @{ML "op THEN"}, which means that @{text "tac THEN"}~@{ML
+  no_tac} is equivalent to @{ML no_tac}.
+
+  \end{description}
+*}
+
+text %mlex {* The following examples illustrate how these primitive
+  tactics can be used to imitate existing combinators like @{ML TRY}
+  or @{ML REPEAT} (ignoring some further implementation tricks):
+*}
+
+ML {*
+  fun TRY tac = tac ORELSE all_tac;
+  fun REPEAT tac st = ((tac THEN REPEAT tac) ORELSE all_tac) st;
+*}
+
+text {* If @{text "tac"} can return multiple outcomes then so can @{ML
+  REPEAT}~@{text "tac"}.  @{ML REPEAT} uses @{ML "op ORELSE"} and not
+  @{ML "op APPEND"}, it applies @{text "tac"} as many times as
+  possible in each outcome.
+
+  \begin{warn}
+  Note @{ML REPEAT}'s explicit abstraction over the proof state.
+  Recursive tacticals must be coded in this awkward fashion to avoid
+  infinite recursion.  With the following definition, @{ML
+  REPEAT}~@{text "tac"} would loop due to the eager evaluation
+  strategy of ML:
+  \end{warn}
+*}
+
+ML {*
+  fun REPEAT tac = (tac THEN REPEAT tac) ORELSE all_tac;  (*BAD!*)
+*}
+
 end

--- a/doc-src/IsarImplementation/Thy/document/Tactic.tex	Wed Jan 25 18:18:59 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex	Wed Jan 25 19:04:38 2012 +0100
@@ -572,7 +572,184 @@
 %
 \endisadelimmlref
 %
+\isamarkupsubsection{Repetition tacticals%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+These tacticals provide further control over repetition of
+  tactics, beyond the stylized forms of ``\verb|?|''  and
+  ``\verb|+|'' in Isar method expressions.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexdef{}{ML}{TRY}\verb|TRY: tactic -> tactic| \\
+  \indexdef{}{ML}{REPEAT\_DETERM}\verb|REPEAT_DETERM: tactic -> tactic| \\
+  \indexdef{}{ML}{REPEAT\_DETERM\_N}\verb|REPEAT_DETERM_N: int -> tactic -> tactic| \\
+  \indexdef{}{ML}{REPEAT}\verb|REPEAT: tactic -> tactic| \\
+  \indexdef{}{ML}{REPEAT1}\verb|REPEAT1: tactic -> tactic| \\
+  \indexdef{}{ML}{DETERM\_UNTIL}\verb|DETERM_UNTIL: (thm -> bool) -> tactic -> tactic| \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item \verb|TRY|~\isa{tac} applies \isa{tac} to the proof
+  state and returns the resulting sequence, if non-empty; otherwise it
+  returns the original state.  Thus, it applies \isa{tac} at most
+  once.
+
+  \item \verb|REPEAT_DETERM|~\isa{tac} applies \isa{tac} to the
+  proof state and, recursively, to the head of the resulting sequence.
+  It returns the first state to make \isa{tac} fail.  It is
+  deterministic, discarding alternative outcomes.
+
+  \item \verb|REPEAT_DETERM_N|~\isa{n\ tac} is like \verb|REPEAT_DETERM|~\isa{tac} but the number of repetitions is bound
+  by \isa{n} (where \verb|~1| means \isa{{\isaliteral{5C3C696E66696E6974793E}{\isasyminfinity}}}).
+
+  \item \verb|REPEAT|~\isa{tac} applies \isa{tac} to the proof
+  state and, recursively, to each element of the resulting sequence.
+  The resulting sequence consists of those states that make \isa{tac} fail.  Thus, it applies \isa{tac} as many times as
+  possible (including zero times), and allows backtracking over each
+  invocation of \isa{tac}.  \verb|REPEAT| is more general than \verb|REPEAT_DETERM|, but requires more space.
+
+  \item \verb|REPEAT1|~\isa{tac} is like \verb|REPEAT|~\isa{tac}
+  but it always applies \isa{tac} at least once, failing if this
+  is impossible.
+
+  \item \verb|DETERM_UNTIL|~\isa{P\ tac} applies \isa{tac} to
+  the proof state and, recursively, to the head of the resulting
+  sequence, until the predicate \isa{P} (applied on the proof
+  state) yields \verb|true|. It fails if \isa{tac} fails on any of
+  the intermediate states. It is deterministic, discarding alternative
+  outcomes.
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isamarkupsubsection{Identities for tacticals%
+}
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexdef{}{ML}{all\_tac}\verb|all_tac: tactic| \\
+  \indexdef{}{ML}{no\_tac}\verb|no_tac: tactic| \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item \verb|all_tac| maps any proof state to the one-element sequence
+  containing that state.  Thus, it succeeds for all states.  It is the
+  identity element of the tactical \verb|op THEN|.
+
+  \item \verb|no_tac| maps any proof state to the empty sequence.  Thus
+  it succeeds for no state.  It is the identity element of
+  \verb|op ORELSE| and \verb|op APPEND|.  Also, it is a zero element
+  for \verb|op THEN|, which means that \isa{tac\ THEN}~\verb|no_tac| is equivalent to \verb|no_tac|.
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isatagmlex
+%
+\begin{isamarkuptext}%
+The following examples illustrate how these primitive
+  tactics can be used to imitate existing combinators like \verb|TRY|
+  or \verb|REPEAT| (ignoring some further implementation tricks):%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlex
+{\isafoldmlex}%
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
+\ \ fun\ TRY\ tac\ {\isaliteral{3D}{\isacharequal}}\ tac\ ORELSE\ all{\isaliteral{5F}{\isacharunderscore}}tac{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\ \ fun\ REPEAT\ tac\ st\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}tac\ THEN\ REPEAT\ tac{\isaliteral{29}{\isacharparenright}}\ ORELSE\ all{\isaliteral{5F}{\isacharunderscore}}tac{\isaliteral{29}{\isacharparenright}}\ st{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+{\isaliteral{2A7D}{\isacharverbatimclose}}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+If \isa{tac} can return multiple outcomes then so can \verb|REPEAT|~\isa{tac}.  \verb|REPEAT| uses \verb|op ORELSE| and not
+  \verb|op APPEND|, it applies \isa{tac} as many times as
+  possible in each outcome.
+
+  \begin{warn}
+  Note \verb|REPEAT|'s explicit abstraction over the proof state.
+  Recursive tacticals must be coded in this awkward fashion to avoid
+  infinite recursion.  With the following definition, \verb|REPEAT|~\isa{tac} would loop due to the eager evaluation
+  strategy of ML:
+  \end{warn}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
+\ \ fun\ REPEAT\ tac\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}tac\ THEN\ REPEAT\ tac{\isaliteral{29}{\isacharparenright}}\ ORELSE\ all{\isaliteral{5F}{\isacharunderscore}}tac{\isaliteral{3B}{\isacharsemicolon}}\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}BAD{\isaliteral{21}{\isacharbang}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
+{\isaliteral{2A7D}{\isacharverbatimclose}}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+\isanewline
+%
 \isadelimtheory
+\isanewline
 %
 \endisadelimtheory
 %

--- a/doc-src/Ref/tctical.tex	Wed Jan 25 18:18:59 2012 +0100
+++ b/doc-src/Ref/tctical.tex	Wed Jan 25 19:04:38 2012 +0100
@@ -1,106 +1,6 @@
 
 \chapter{Tacticals}
 
-\section{The basic tacticals}
-
-\subsection{Repetition tacticals}
-\index{tacticals!repetition}
-\begin{ttbox} 
-TRY             : tactic -> tactic
-REPEAT_DETERM   : tactic -> tactic
-REPEAT_DETERM_N : int -> tactic -> tactic
-REPEAT          : tactic -> tactic
-REPEAT1         : tactic -> tactic
-DETERM_UNTIL    : (thm -> bool) -> tactic -> tactic
-trace_REPEAT    : bool ref \hfill{\bf initially false}
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{TRY} {\it tac}] 
-applies {\it tac\/} to the proof state and returns the resulting sequence,
-if non-empty; otherwise it returns the original state.  Thus, it applies
-{\it tac\/} at most once.
-
-\item[\ttindexbold{REPEAT_DETERM} {\it tac}] 
-applies {\it tac\/} to the proof state and, recursively, to the head of the
-resulting sequence.  It returns the first state to make {\it tac\/} fail.
-It is deterministic, discarding alternative outcomes.
-
-\item[\ttindexbold{REPEAT_DETERM_N} {\it n} {\it tac}] 
-is like \hbox{\tt REPEAT_DETERM {\it tac}} but the number of repititions
-is bound by {\it n} (unless negative).
-
-\item[\ttindexbold{REPEAT} {\it tac}] 
-applies {\it tac\/} to the proof state and, recursively, to each element of
-the resulting sequence.  The resulting sequence consists of those states
-that make {\it tac\/} fail.  Thus, it applies {\it tac\/} as many times as
-possible (including zero times), and allows backtracking over each
-invocation of {\it tac}.  It is more general than {\tt REPEAT_DETERM}, but
-requires more space.
-
-\item[\ttindexbold{REPEAT1} {\it tac}] 
-is like \hbox{\tt REPEAT {\it tac}} but it always applies {\it tac\/} at
-least once, failing if this is impossible.
-
-\item[\ttindexbold{DETERM_UNTIL} {\it p} {\it tac}] 
-applies {\it tac\/} to the proof state and, recursively, to the head of the
-resulting sequence, until the predicate {\it p} (applied on the proof state)
-yields {\it true}. It fails if {\it tac\/} fails on any of the intermediate 
-states. It is deterministic, discarding alternative outcomes.
-
-\item[set \ttindexbold{trace_REPEAT};] 
-enables an interactive tracing mode for the tacticals {\tt REPEAT_DETERM}
-and {\tt REPEAT}.  To view the tracing options, type {\tt h} at the prompt.
-\end{ttdescription}
-
-
-\subsection{Identities for tacticals}
-\index{tacticals!identities for}
-\begin{ttbox} 
-all_tac : tactic
-no_tac  : tactic
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{all_tac}] 
-maps any proof state to the one-element sequence containing that state.
-Thus, it succeeds for all states.  It is the identity element of the
-tactical \ttindex{THEN}\@.
-
-\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}, 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,
-\ttindexbold{TRY} and \ttindexbold{REPEAT} (ignoring tracing) can be coded
-as follows: 
-\begin{ttbox} 
-fun TRY tac = tac ORELSE all_tac;
-
-fun REPEAT tac =
-     (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}, it
-applies $tac$ as many times as possible in each outcome.
-
-\begin{warn}
-Note {\tt REPEAT}'s explicit abstraction over the proof state.  Recursive
-tacticals must be coded in this awkward fashion to avoid infinite
-recursion.  With the following definition, \hbox{\tt REPEAT $tac$} would
-loop due to \ML's eager evaluation strategy:
-\begin{ttbox} 
-fun REPEAT tac = (tac THEN REPEAT tac) ORELSE all_tac;
-\end{ttbox}
-\par\noindent
-The built-in {\tt REPEAT} avoids~{\tt THEN}, handling sequences explicitly
-and using tail recursion.  This sacrifices clarity, but saves much space by
-discarding intermediate proof states.
-\end{warn}
-
-
 \section{Control and search tacticals}
 \index{search!tacticals|(}