1.1 --- a/doc-src/IsarRef/Thy/Generic.thy	Mon Jun 16 11:47:46 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Generic.thy	Mon Jun 16 14:18:45 2008 +0200
     1.3 @@ -284,6 +284,7 @@
     1.4      @{method_def rename_tac}@{text "\<^sup>*"} & : & \isarmeth \\
     1.5      @{method_def rotate_tac}@{text "\<^sup>*"} & : & \isarmeth \\
     1.6      @{method_def tactic}@{text "\<^sup>*"} & : & \isarmeth \\
     1.7 +    @{method_def raw_tactic}@{text "\<^sup>*"} & : & \isarmeth \\
     1.8    \end{matharray}
     1.9  
    1.10    \begin{rail}
    1.11 @@ -296,7 +297,7 @@
    1.12      ;
    1.13      'rotate\_tac' goalspec? int?
    1.14      ;
    1.15 -    'tactic' text
    1.16 +    ('tactic' | 'raw_tactic') text
    1.17      ;
    1.18  
    1.19      insts: ((name '=' term) + 'and') 'in'
    1.20 @@ -341,21 +342,16 @@
    1.21  
    1.22    \item [@{method tactic}~@{text "text"}] produces a proof method from
    1.23    any ML text of type @{ML_type tactic}.  Apart from the usual ML
    1.24 -  environment and the current implicit theory context, the ML code may
    1.25 -  refer to the following locally bound values:
    1.26 +  environment and the current proof context, the ML code may refer to
    1.27 +  the locally bound values @{ML_text facts}, which indicates any
    1.28 +  current facts used for forward-chaining.
    1.29  
    1.30 -%FIXME check
    1.31 -{\footnotesize\begin{verbatim}
    1.32 -val ctxt  : Proof.context
    1.33 -val facts : thm list
    1.34 -val thm   : string -> thm
    1.35 -val thms  : string -> thm list
    1.36 -\end{verbatim}}
    1.37 -
    1.38 -  Here @{ML_text ctxt} refers to the current proof context, @{ML_text
    1.39 -  facts} indicates any current facts for forward-chaining, and @{ML
    1.40 -  thm}~/~@{ML thms} retrieve named facts (including global theorems)
    1.41 -  from the context.
    1.42 +  \item [@{method raw_tactic}] is similar to @{method tactic}, but
    1.43 +  presents the goal state in its raw internal form, where simultaneous
    1.44 +  subgoals appear as conjunction of the logical framework instead of
    1.45 +  the usual split into several subgoals.  While feature this is useful
    1.46 +  for debugging of complex method definitions, it should not never
    1.47 +  appear in production theories.
    1.48  
    1.49    \end{descr}
    1.50  *}