--- 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).