# HG changeset patch
# User wenzelm
# Date 1226608800 -3600
# Node ID 7f7002ad6289978ca5d113822d28e1218604ce11
# Parent  529798e7192404653504ef9ec91b61fba1edcacc
tuned section "Incorporating ML code";
moved method_setup to separate section "Defining proof methods";

diff -r 529798e71924 -r 7f7002ad6289 doc-src/IsarRef/Thy/Proof.thy
--- a/doc-src/IsarRef/Thy/Proof.thy	Thu Nov 13 21:38:44 2008 +0100
+++ b/doc-src/IsarRef/Thy/Proof.thy	Thu Nov 13 21:40:00 2008 +0100
@@ -796,7 +796,7 @@
   
   \item [@{attribute OF}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] applies some
   theorem to all of the given rules @{text "a\<^sub>1, \<dots>, a\<^sub>n"}
-  (in parallel).  This corresponds to the @{ML "op MRS"} operation in
+  (in parallel).  This corresponds to the @{ML  [source=false] "op MRS"} operation in
   ML, but note the reversed order.  Positions may be effectively
   skipped by including ``@{text _}'' (underscore) as argument.
   
@@ -897,6 +897,50 @@
 *}
 
 
+subsection {* Defining proof methods *}
+
+text {*
+  \begin{matharray}{rcl}
+    @{command_def "method_setup"} & : & \isartrans{theory}{theory} \\
+  \end{matharray}
+
+  \begin{rail}
+    'method\_setup' name '=' text text
+    ;
+  \end{rail}
+
+  \begin{descr}
+
+  \item [@{command "method_setup"}~@{text "name = text description"}]
+  defines a proof method in the current theory.  The given @{text
+  "text"} has to be an ML expression of type @{ML_type [source=false]
+  "Args.src -> Proof.context -> Proof.method"}.  Parsing concrete
+  method syntax from @{ML_type Args.src} input can be quite tedious in
+  general.  The following simple examples are for methods without any
+  explicit arguments, or a list of theorems, respectively.
+
+%FIXME proper antiquotations
+{\footnotesize
+\begin{verbatim}
+ Method.no_args (Method.METHOD (fn facts => foobar_tac))
+ Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac))
+ Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac))
+ Method.thms_ctxt_args (fn thms => fn ctxt =>
+    Method.METHOD (fn facts => foobar_tac))
+\end{verbatim}
+}
+
+  Note that mere tactic emulations may ignore the @{text facts}
+  parameter above.  Proper proof methods would do something
+  appropriate with the list of current facts, though.  Single-rule
+  methods usually do strict forward-chaining (e.g.\ by using @{ML
+  Drule.multi_resolves}), while automatic ones just insert the facts
+  using @{ML Method.insert_tac} before applying the main tactic.
+
+  \end{descr}
+*}
+
+
 section {* Generalized elimination \label{sec:obtain} *}
 
 text {*
diff -r 529798e71924 -r 7f7002ad6289 doc-src/IsarRef/Thy/Spec.thy
--- a/doc-src/IsarRef/Thy/Spec.thy	Thu Nov 13 21:38:44 2008 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy	Thu Nov 13 21:40:00 2008 +0100
@@ -808,15 +808,12 @@
     @{command_def "ML_val"} & : & \isartrans{\cdot}{\cdot} \\
     @{command_def "ML_command"} & : & \isartrans{\cdot}{\cdot} \\
     @{command_def "setup"} & : & \isartrans{theory}{theory} \\
-    @{command_def "method_setup"} & : & \isartrans{theory}{theory} \\
   \end{matharray}
 
   \begin{rail}
     'use' name
     ;
-    ('ML' | 'ML\_val' | 'ML\_command' | 'setup') text
-    ;
-    'method\_setup' name '=' text text
+    ('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup') text
     ;
   \end{rail}
 
@@ -824,7 +821,7 @@
 
   \item [@{command "use"}~@{text "file"}] reads and executes ML
   commands from @{text "file"}.  The current theory context is passed
-  down to the ML toplevel and may be modified, using @{ML
+  down to the ML toplevel and may be modified, using @{ML [source=false]
   "Context.>>"} or derived ML commands.  The file name is checked with
   the @{keyword_ref "uses"} dependency declaration given in the theory
   header (see also \secref{sec:begin-thy}).
@@ -852,36 +849,10 @@
   
   \item [@{command "setup"}~@{text "text"}] changes the current theory
   context by applying @{text "text"}, which refers to an ML expression
-  of type @{ML_type "theory -> theory"}.  This enables to initialize
-  any object-logic specific tools and packages written in ML, for
-  example.
+  of type @{ML_type [source=false] "theory -> theory"}.  This enables
+  to initialize any object-logic specific tools and packages written
+  in ML, for example.
   
-  \item [@{command "method_setup"}~@{text "name = text description"}]
-  defines a proof method in the current theory.  The given @{text
-  "text"} has to be an ML expression of type @{ML_type "Args.src ->
-  Proof.context -> Proof.method"}.  Parsing concrete method syntax
-  from @{ML_type Args.src} input can be quite tedious in general.  The
-  following simple examples are for methods without any explicit
-  arguments, or a list of theorems, respectively.
-
-%FIXME proper antiquotations
-{\footnotesize
-\begin{verbatim}
- Method.no_args (Method.METHOD (fn facts => foobar_tac))
- Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac))
- Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac))
- Method.thms_ctxt_args (fn thms => fn ctxt =>
-    Method.METHOD (fn facts => foobar_tac))
-\end{verbatim}
-}
-
-  Note that mere tactic emulations may ignore the @{text facts}
-  parameter above.  Proper proof methods would do something
-  appropriate with the list of current facts, though.  Single-rule
-  methods usually do strict forward-chaining (e.g.\ by using @{ML
-  Drule.multi_resolves}), while automatic ones just insert the facts
-  using @{ML Method.insert_tac} before applying the main tactic.
-
   \end{descr}
 *}