diff -r 8f1f33faf24e -r aea65ff733b4 doc-src/IsarImplementation/Thy/document/Tactic.tex
--- 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).