--- 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}
*}
--- 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}%