# HG changeset patch
# User wenzelm
# Date 1327586675 -3600
# Node ID f575281fb551ba02aa8b20f57b0510ea4f850228
# Parent  a87e06a18a5c46d12b1d9fb83f47050ce04c874e
tuned;

diff -r a87e06a18a5c -r f575281fb551 doc-src/IsarImplementation/Thy/Tactic.thy
--- a/doc-src/IsarImplementation/Thy/Tactic.thy	Wed Jan 25 22:01:15 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/Tactic.thy	Thu Jan 26 15:04:35 2012 +0100
@@ -433,8 +433,6 @@
   @{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}
@@ -471,18 +469,12 @@
   "tac\<^sub>n"}.  Note that @{ML "FIRST []"} is the same as @{ML no_tac}: it
   always fails.
 
-  \item @{ML_op "THEN'"}, @{ML_op "ORELSE'"}, and @{ML_op "APPEND'"}
-  are lifted versions of @{ML_op "THEN"}, @{ML_op "ORELSE"}, and
-  @{ML_op "APPEND"}, for tactics with explicit subgoal addressing.
-  This means @{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)"} etc.
+  \item @{ML_op "THEN'"} is the lifted version of @{ML_op "THEN"}, for
+  tactics with explicit subgoal addressing.  Thus @{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)"}.
 
-  \item @{ML "EVERY'"} and @{ML "FIRST'"} are lifted versions of @{ML
-  "EVERY'"} and @{ML "FIRST'"}, for tactics with explicit subgoal
-  addressing.
-
-  \item @{ML "EVERY1"} and @{ML "FIRST1"} are convenience versions of
-  @{ML "EVERY'"} and @{ML "FIRST'"}, applied to subgoal 1.
+  The other primed tacticals work analogously.
 
   \end{description}
 *}
diff -r a87e06a18a5c -r f575281fb551 doc-src/IsarImplementation/Thy/document/Tactic.tex
--- a/doc-src/IsarImplementation/Thy/document/Tactic.tex	Wed Jan 25 22:01:15 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex	Thu Jan 26 15:04:35 2012 +0100
@@ -520,8 +520,6 @@
   \indexdef{}{ML infix}{APPEND'}\verb|infix 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}
@@ -554,17 +552,10 @@
   \item \verb|FIRST|~\isa{{\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}}}~\verb|ORELSE|~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb|ORELSE|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n}.  Note that \verb|FIRST []| is the same as \verb|no_tac|: it
   always fails.
 
-  \item \verb|THEN'|, \verb|ORELSE'|, and \verb|APPEND'|
-  are lifted versions of \verb|THEN|, \verb|ORELSE|, and
-  \verb|APPEND|, for tactics with explicit subgoal addressing.
-  This means \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}}} etc.
+  \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}}}.
 
-  \item \verb|EVERY'| and \verb|FIRST'| are lifted versions of \verb|EVERY'| and \verb|FIRST'|, for tactics with explicit subgoal
-  addressing.
-
-  \item \verb|EVERY1| and \verb|FIRST1| are convenience versions of
-  \verb|EVERY'| and \verb|FIRST'|, applied to subgoal 1.
+  The other primed tacticals work analogously.
 
   \end{description}%
 \end{isamarkuptext}%