--- a/doc-src/IsarImplementation/Thy/Tactic.thy Thu Jan 26 22:21:33 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/Tactic.thy Fri Jan 27 21:29:37 2012 +0100
@@ -364,7 +364,8 @@
@{index_ML res_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\
@{index_ML eres_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\
@{index_ML dres_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\
- @{index_ML forw_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\[1ex]
+ @{index_ML forw_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\
+ @{index_ML subgoal_tac: "Proof.context -> string -> int -> tactic"} \\
@{index_ML rename_tac: "string list -> int -> tactic"} \\
\end{mldecls}
@@ -383,6 +384,10 @@
\item @{ML forw_inst_tac} is like @{ML dres_inst_tac} except that
the selected assumption is not deleted.
+ \item @{ML subgoal_tac}~@{text "ctxt \<phi> i"} adds the proposition
+ @{text "\<phi>"} as local premise to subgoal @{text "i"}, and poses the
+ same as a new subgoal @{text "i + 1"} (in the original context).
+
\item @{ML rename_tac}~@{text "names i"} renames the innermost
parameters of subgoal @{text i} according to the provided @{text
names} (which need to be distinct indentifiers).
--- a/doc-src/IsarImplementation/Thy/document/Tactic.tex Thu Jan 26 22:21:33 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex Fri Jan 27 21:29:37 2012 +0100
@@ -432,7 +432,8 @@
\indexdef{}{ML}{res\_inst\_tac}\verb|res_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\
\indexdef{}{ML}{eres\_inst\_tac}\verb|eres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\
\indexdef{}{ML}{dres\_inst\_tac}\verb|dres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\
- \indexdef{}{ML}{forw\_inst\_tac}\verb|forw_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\[1ex]
+ \indexdef{}{ML}{forw\_inst\_tac}\verb|forw_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\
+ \indexdef{}{ML}{subgoal\_tac}\verb|subgoal_tac: Proof.context -> string -> int -> tactic| \\
\indexdef{}{ML}{rename\_tac}\verb|rename_tac: string list -> int -> tactic| \\
\end{mldecls}
@@ -451,6 +452,10 @@
\item \verb|forw_inst_tac| is like \verb|dres_inst_tac| except that
the selected assumption is not deleted.
+ \item \verb|subgoal_tac|~\isa{ctxt\ {\isaliteral{5C3C7068693E}{\isasymphi}}\ i} adds the proposition
+ \isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} as local premise to subgoal \isa{i}, and poses the
+ same as a new subgoal \isa{i\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}} (in the original context).
+
\item \verb|rename_tac|~\isa{names\ i} renames the innermost
parameters of subgoal \isa{i} according to the provided \isa{names} (which need to be distinct indentifiers).
--- a/doc-src/IsarRef/Thy/Generic.thy Thu Jan 26 22:21:33 2012 +0100
+++ b/doc-src/IsarRef/Thy/Generic.thy Fri Jan 27 21:29:37 2012 +0100
@@ -339,9 +339,9 @@
from a subgoal; note that @{text \<phi>} may contain schematic variables.
See also @{ML thin_tac} in \cite{isabelle-implementation}.
- \item @{method subgoal_tac}~@{text \<phi>} adds @{text \<phi>} as an
- assumption to a subgoal. See also @{ML subgoal_tac} and @{ML
- subgoals_tac} in \cite{isabelle-implementation}.
+ \item @{method subgoal_tac}~@{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} adds the propositions
+ @{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} as local premises to a subgoal, and poses the same
+ as new subgoals (in the original context).
\item @{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"} renames parameters of a
goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the
--- a/doc-src/IsarRef/Thy/document/Generic.tex Thu Jan 26 22:21:33 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/Generic.tex Fri Jan 27 21:29:37 2012 +0100
@@ -541,8 +541,9 @@
from a subgoal; note that \isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} may contain schematic variables.
See also \verb|thin_tac| in \cite{isabelle-implementation}.
- \item \hyperlink{method.subgoal-tac}{\mbox{\isa{subgoal{\isaliteral{5F}{\isacharunderscore}}tac}}}~\isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} adds \isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} as an
- assumption to a subgoal. See also \verb|subgoal_tac| and \verb|subgoals_tac| in \cite{isabelle-implementation}.
+ \item \hyperlink{method.subgoal-tac}{\mbox{\isa{subgoal{\isaliteral{5F}{\isacharunderscore}}tac}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} adds the propositions
+ \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} as local premises to a subgoal, and poses the same
+ as new subgoals (in the original context).
\item \hyperlink{method.rename-tac}{\mbox{\isa{rename{\isaliteral{5F}{\isacharunderscore}}tac}}}~\isa{{\isaliteral{22}{\isachardoublequote}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} renames parameters of a
goal according to the list \isa{{\isaliteral{22}{\isachardoublequote}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}, which refers to the
--- a/doc-src/Ref/tactic.tex Thu Jan 26 22:21:33 2012 +0100
+++ b/doc-src/Ref/tactic.tex Fri Jan 27 21:29:37 2012 +0100
@@ -9,8 +9,6 @@
\begin{ttbox}
cut_facts_tac : thm list -> int -> tactic
cut_inst_tac : (string*string)list -> thm -> int -> tactic
-subgoal_tac : string -> int -> tactic
-subgoals_tac : string list -> int -> tactic
\end{ttbox}
These tactics add assumptions to a subgoal.
\begin{ttdescription}
@@ -28,13 +26,6 @@
described in {\S}\ref{res_inst_tac}. It adds the resulting theorem as a
new assumption to subgoal~$i$.
-\item[\ttindexbold{subgoal_tac} {\it formula} {\it i}]
-adds the {\it formula} as an assumption to subgoal~$i$, and inserts the same
-{\it formula} as a new subgoal, $i+1$.
-
-\item[\ttindexbold{subgoals_tac} {\it formulae} {\it i}]
- uses {\tt subgoal_tac} to add the members of the list of {\it
- formulae} as assumptions to subgoal~$i$.
\end{ttdescription}
@@ -91,8 +82,7 @@
\item[\tdx{cut_rl}]
is $\List{\psi\Imp\theta,\psi}\Imp\theta$. It is useful for inserting
-assumptions; it underlies {\tt forward_tac}, {\tt cut_facts_tac}
-and {\tt subgoal_tac}.
+assumptions; it underlies {\tt forward_tac}, {\tt cut_facts_tac}.
\end{ttdescription}