# HG changeset patch
# User wenzelm
# Date 1330353587 -3600
# Node ID 877d5797542766a7a57008d1bd9245b9842d2c14
# Parent  88f3f5e01d82af0a7152096e4e36ccf3bce44339
updated cut_tac, without loose references to implementation manual;

diff -r 88f3f5e01d82 -r 877d57975427 doc-src/IsarRef/Thy/Generic.thy
--- a/doc-src/IsarRef/Thy/Generic.thy	Mon Feb 27 15:36:24 2012 +0100
+++ b/doc-src/IsarRef/Thy/Generic.thy	Mon Feb 27 15:39:47 2012 +0100
@@ -329,11 +329,11 @@
   \cite{isabelle-implementation}).
 
   \item @{method cut_tac} inserts facts into the proof state as
-  assumption of a subgoal, see also @{ML Tactic.cut_facts_tac} in
-  \cite{isabelle-implementation}.  Note that the scope of schematic
-  variables is spread over the main goal statement.  Instantiations
-  may be given as well, see also ML tactic @{ML cut_inst_tac} in
-  \cite{isabelle-implementation}.
+  assumption of a subgoal; instantiations may be given as well.  Note
+  that the scope of schematic variables is spread over the main goal
+  statement and rule premises are turned into new subgoals.  This is
+  in contrast to the regular method @{method insert} which inserts
+  closed rule statements.
 
   \item @{method thin_tac}~@{text \<phi>} deletes the specified premise
   from a subgoal.  Note that @{text \<phi>} may contain schematic
diff -r 88f3f5e01d82 -r 877d57975427 doc-src/IsarRef/Thy/document/Generic.tex
--- a/doc-src/IsarRef/Thy/document/Generic.tex	Mon Feb 27 15:36:24 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/Generic.tex	Mon Feb 27 15:39:47 2012 +0100
@@ -531,11 +531,11 @@
   \cite{isabelle-implementation}).
 
   \item \hyperlink{method.cut-tac}{\mbox{\isa{cut{\isaliteral{5F}{\isacharunderscore}}tac}}} inserts facts into the proof state as
-  assumption of a subgoal, see also \verb|Tactic.cut_facts_tac| in
-  \cite{isabelle-implementation}.  Note that the scope of schematic
-  variables is spread over the main goal statement.  Instantiations
-  may be given as well, see also ML tactic \verb|cut_inst_tac| in
-  \cite{isabelle-implementation}.
+  assumption of a subgoal; instantiations may be given as well.  Note
+  that the scope of schematic variables is spread over the main goal
+  statement and rule premises are turned into new subgoals.  This is
+  in contrast to the regular method \hyperlink{method.insert}{\mbox{\isa{insert}}} which inserts
+  closed rule statements.
 
   \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