# 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} *}