# HG changeset patch
# User wenzelm
# Date 1213618735 -7200
# Node ID ac158759125cb7e5e976a71e6d48321216e373de
# Parent  8546e2407b31b11d205a84e348770406436c2c00
updated generated file;

diff -r 8546e2407b31 -r ac158759125c doc-src/IsarRef/Thy/document/Generic.tex
--- a/doc-src/IsarRef/Thy/document/Generic.tex	Mon Jun 16 14:18:45 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex	Mon Jun 16 14:18:55 2008 +0200
@@ -302,6 +302,7 @@
     \indexdef{}{method}{rename\_tac}\hypertarget{method.rename-tac}{\hyperlink{method.rename-tac}{\mbox{\isa{rename{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
     \indexdef{}{method}{rotate\_tac}\hypertarget{method.rotate-tac}{\hyperlink{method.rotate-tac}{\mbox{\isa{rotate{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
     \indexdef{}{method}{tactic}\hypertarget{method.tactic}{\hyperlink{method.tactic}{\mbox{\isa{tactic}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
+    \indexdef{}{method}{raw\_tactic}\hypertarget{method.raw-tactic}{\hyperlink{method.raw-tactic}{\mbox{\isa{raw{\isacharunderscore}tactic}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
   \end{matharray}
 
   \begin{rail}
@@ -314,7 +315,7 @@
     ;
     'rotate\_tac' goalspec? int?
     ;
-    'tactic' text
+    ('tactic' | 'raw_tactic') text
     ;
 
     insts: ((name '=' term) + 'and') 'in'
@@ -356,19 +357,16 @@
 
   \item [\hyperlink{method.tactic}{\mbox{\isa{tactic}}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] produces a proof method from
   any ML text of type \verb|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 \verb|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 \verb|ctxt| refers to the current proof context, \verb|facts| indicates any current facts for forward-chaining, and \verb|thm|~/~\verb|thms| retrieve named facts (including global theorems)
-  from the context.
+  \item [\hyperlink{method.raw-tactic}{\mbox{\isa{raw{\isacharunderscore}tactic}}}] is similar to \hyperlink{method.tactic}{\mbox{\isa{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}%
 \end{isamarkuptext}%