# HG changeset patch
# User wenzelm
# Date 1327588151 -3600
# Node ID a9694a4e39e543033e23523bb190c46061325f14
# Parent  b6ab3cdea1637a179256867c3c3b34639744437c
removed some obscure material;
misc tuning;

diff -r b6ab3cdea163 -r a9694a4e39e5 doc-src/IsarImplementation/Thy/Tactic.thy
--- a/doc-src/IsarImplementation/Thy/Tactic.thy	Thu Jan 26 15:28:17 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/Tactic.thy	Thu Jan 26 15:29:11 2012 +0100
@@ -470,7 +470,7 @@
   always fails.
 
   \item @{ML_op "THEN'"} is the lifted version of @{ML_op "THEN"}, for
-  tactics with explicit subgoal addressing.  Thus @{text
+  tactics with explicit subgoal addressing.  So @{text
   "(tac\<^sub>1"}~@{ML_op THEN'}~@{text "tac\<^sub>2) i"} is the same as @{text
   "(tac\<^sub>1 i"}~@{ML_op THEN}~@{text "tac\<^sub>2 i)"}.
 
@@ -489,11 +489,10 @@
 text %mlref {*
   \begin{mldecls}
   @{index_ML "TRY": "tactic -> tactic"} \\
+  @{index_ML "REPEAT": "tactic -> tactic"} \\
+  @{index_ML "REPEAT1": "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}
@@ -503,14 +502,9 @@
   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>"}).
+  Note that for tactics with subgoal addressing, the combinator can be
+  applied via functional composition: @{ML "TRY"}~@{ML_op o}~@{text
+  "tac"}.  There is no need for @{verbatim TRY'}.
 
   \item @{ML REPEAT}~@{text "tac"} applies @{text "tac"} to the proof
   state and, recursively, to each element of the resulting sequence.
@@ -524,12 +518,14 @@
   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.
+  \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>"}).
 
   \end{description}
 *}
@@ -592,18 +588,15 @@
   @{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.  *}
+  where a different order is desired. *}
 
 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}
@@ -612,10 +605,6 @@
   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.
@@ -630,13 +619,6 @@
   \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}
 *}
 
diff -r b6ab3cdea163 -r a9694a4e39e5 doc-src/IsarImplementation/Thy/document/Tactic.tex
--- a/doc-src/IsarImplementation/Thy/document/Tactic.tex	Thu Jan 26 15:28:17 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex	Thu Jan 26 15:29:11 2012 +0100
@@ -553,7 +553,7 @@
   always fails.
 
   \item \verb|THEN'| is the lifted version of \verb|THEN|, for
-  tactics with explicit subgoal addressing.  Thus \isa{{\isaliteral{28}{\isacharparenleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verb|THEN'|~\isa{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}~\verb|THEN|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ i{\isaliteral{29}{\isacharparenright}}}.
+  tactics with explicit subgoal addressing.  So \isa{{\isaliteral{28}{\isacharparenleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verb|THEN'|~\isa{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}~\verb|THEN|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ i{\isaliteral{29}{\isacharparenright}}}.
 
   The other primed tacticals work analogously.
 
@@ -588,11 +588,10 @@
 \begin{isamarkuptext}%
 \begin{mldecls}
   \indexdef{}{ML}{TRY}\verb|TRY: tactic -> tactic| \\
+  \indexdef{}{ML}{REPEAT}\verb|REPEAT: tactic -> tactic| \\
+  \indexdef{}{ML}{REPEAT1}\verb|REPEAT1: 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}
@@ -602,13 +601,8 @@
   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}}}).
+  Note that for tactics with subgoal addressing, the combinator can be
+  applied via functional composition: \verb|TRY|~\verb|o|~\isa{tac}.  There is no need for \verb|TRY'|.
 
   \item \verb|REPEAT|~\isa{tac} applies \isa{tac} to the proof
   state and, recursively, to each element of the resulting sequence.
@@ -620,12 +614,13 @@
   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.
+  \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}}}).
 
   \end{description}%
 \end{isamarkuptext}%
@@ -736,8 +731,7 @@
   \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.%
+  where a different order is desired.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -750,12 +744,10 @@
 \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}
@@ -763,8 +755,6 @@
   \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.
 
@@ -777,12 +767,6 @@
   \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%