--- a/doc-src/IsarImplementation/Thy/Tactic.thy Sun Jan 29 21:40:29 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/Tactic.thy Sun Jan 29 22:00:10 2012 +0100
@@ -366,6 +366,7 @@
@{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"} \\
@{index_ML subgoal_tac: "Proof.context -> string -> int -> tactic"} \\
+ @{index_ML thin_tac: "Proof.context -> string -> int -> tactic"} \\
@{index_ML rename_tac: "string list -> int -> tactic"} \\
\end{mldecls}
@@ -388,6 +389,13 @@
@{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 thin_tac}~@{text "ctxt \<phi> i"} deletes the specified
+ premise from subgoal @{text i}. Note that @{text \<phi>} may contain
+ schematic variables, to abbreviate the intended proposition; the
+ first matching subgoal premise will be deleted. Removing useless
+ premises from a subgoal increases its readability and can make
+ search tactics run faster.
+
\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 Sun Jan 29 21:40:29 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex Sun Jan 29 22:00:10 2012 +0100
@@ -434,6 +434,7 @@
\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| \\
\indexdef{}{ML}{subgoal\_tac}\verb|subgoal_tac: Proof.context -> string -> int -> tactic| \\
+ \indexdef{}{ML}{thin\_tac}\verb|thin_tac: Proof.context -> string -> int -> tactic| \\
\indexdef{}{ML}{rename\_tac}\verb|rename_tac: string list -> int -> tactic| \\
\end{mldecls}
@@ -456,6 +457,13 @@
\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|thin_tac|~\isa{ctxt\ {\isaliteral{5C3C7068693E}{\isasymphi}}\ i} deletes the specified
+ premise from subgoal \isa{i}. Note that \isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} may contain
+ schematic variables, to abbreviate the intended proposition; the
+ first matching subgoal premise will be deleted. Removing useless
+ premises from a subgoal increases its readability and can make
+ search tactics run faster.
+
\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 Sun Jan 29 21:40:29 2012 +0100
+++ b/doc-src/IsarRef/Thy/Generic.thy Sun Jan 29 22:00:10 2012 +0100
@@ -335,9 +335,12 @@
may be given as well, see also ML tactic @{ML cut_inst_tac} in
\cite{isabelle-implementation}.
- \item @{method thin_tac}~@{text \<phi>} deletes the specified assumption
- from a subgoal; note that @{text \<phi>} may contain schematic variables.
- See also @{ML thin_tac} in \cite{isabelle-implementation}.
+ \item @{method thin_tac}~@{text \<phi>} deletes the specified premise
+ from a subgoal. Note that @{text \<phi>} may contain schematic
+ variables, to abbreviate the intended proposition; the first
+ matching subgoal premise will be deleted. Removing useless premises
+ from a subgoal increases its readability and can make search tactics
+ run faster.
\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
--- a/doc-src/IsarRef/Thy/document/Generic.tex Sun Jan 29 21:40:29 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/Generic.tex Sun Jan 29 22:00:10 2012 +0100
@@ -537,9 +537,12 @@
may be given as well, see also ML tactic \verb|cut_inst_tac| in
\cite{isabelle-implementation}.
- \item \hyperlink{method.thin-tac}{\mbox{\isa{thin{\isaliteral{5F}{\isacharunderscore}}tac}}}~\isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} deletes the specified assumption
- 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.thin-tac}{\mbox{\isa{thin{\isaliteral{5F}{\isacharunderscore}}tac}}}~\isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} deletes the specified premise
+ from a subgoal. Note that \isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} may contain schematic
+ variables, to abbreviate the intended proposition; the first
+ matching subgoal premise will be deleted. Removing useless premises
+ from a subgoal increases its readability and can make search tactics
+ run faster.
\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
--- a/doc-src/Ref/tactic.tex Sun Jan 29 21:40:29 2012 +0100
+++ b/doc-src/Ref/tactic.tex Sun Jan 29 22:00:10 2012 +0100
@@ -84,21 +84,6 @@
\section{Obscure tactics}
-\subsection{Manipulating assumptions}
-\begin{ttbox}
-thin_tac : string -> int -> tactic
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{thin_tac} {\it formula} $i$]
-\index{assumptions!deleting}
-deletes the specified assumption from subgoal $i$. Often the assumption
-can be abbreviated, replacing subformul{\ae} by unknowns; the first matching
-assumption will be deleted. Removing useless assumptions from a subgoal
-increases its readability and can make search tactics run faster.
-
-\end{ttdescription}
-
-
\subsection{Composition: resolution without lifting}
\index{tactics!for composition}
\begin{ttbox}