# HG changeset patch
# User wenzelm
# Date 1327870810 -3600
# Node ID aea65ff733b4068ec299ff81e92bc0f68a0f51ae
# Parent  8f1f33faf24e9ee2b632f5662875edfd2ca75b8d
updated thin_tac;

diff -r 8f1f33faf24e -r aea65ff733b4 doc-src/IsarImplementation/Thy/Tactic.thy
--- 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).
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).
 
diff -r 8f1f33faf24e -r aea65ff733b4 doc-src/IsarRef/Thy/Generic.thy
--- 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
diff -r 8f1f33faf24e -r aea65ff733b4 doc-src/IsarRef/Thy/document/Generic.tex
--- 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
diff -r 8f1f33faf24e -r aea65ff733b4 doc-src/Ref/tactic.tex
--- 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}