# HG changeset patch
# User wenzelm
# Date 1213618725 -7200
# Node ID 8546e2407b31b11d205a84e348770406436c2c00
# Parent  b08abdb8f4995b936bd8308df58cd5a9c4211363
method "tactic": only "facts" as bound value;
added method "raw_tactic";

diff -r b08abdb8f499 -r 8546e2407b31 doc-src/IsarRef/Thy/Generic.thy
--- a/doc-src/IsarRef/Thy/Generic.thy	Mon Jun 16 11:47:46 2008 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy	Mon Jun 16 14:18:45 2008 +0200
@@ -284,6 +284,7 @@
     @{method_def rename_tac}@{text "\<^sup>*"} & : & \isarmeth \\
     @{method_def rotate_tac}@{text "\<^sup>*"} & : & \isarmeth \\
     @{method_def tactic}@{text "\<^sup>*"} & : & \isarmeth \\
+    @{method_def raw_tactic}@{text "\<^sup>*"} & : & \isarmeth \\
   \end{matharray}
 
   \begin{rail}
@@ -296,7 +297,7 @@
     ;
     'rotate\_tac' goalspec? int?
     ;
-    'tactic' text
+    ('tactic' | 'raw_tactic') text
     ;
 
     insts: ((name '=' term) + 'and') 'in'
@@ -341,21 +342,16 @@
 
   \item [@{method tactic}~@{text "text"}] produces a proof method from
   any ML text of type @{ML_type tactic}.  Apart from the usual ML
-  environment and the current implicit theory context, the ML code may
-  refer to the following locally bound values:
+  environment and the current proof context, the ML code may refer to
+  the locally bound values @{ML_text facts}, which indicates any
+  current facts used for forward-chaining.
 
-%FIXME check
-{\footnotesize\begin{verbatim}
-val ctxt  : Proof.context
-val facts : thm list
-val thm   : string -> thm
-val thms  : string -> thm list
-\end{verbatim}}
-
-  Here @{ML_text ctxt} refers to the current proof context, @{ML_text
-  facts} indicates any current facts for forward-chaining, and @{ML
-  thm}~/~@{ML thms} retrieve named facts (including global theorems)
-  from the context.
+  \item [@{method raw_tactic}] is similar to @{method tactic}, but
+  presents the goal state in its raw internal form, where simultaneous
+  subgoals appear as conjunction of the logical framework instead of
+  the usual split into several subgoals.  While feature this is useful
+  for debugging of complex method definitions, it should not never
+  appear in production theories.
 
   \end{descr}
 *}