# HG changeset patch
# User wenzelm
# Date 1237222267 -3600
# Node ID 4c25146258732176ebdd15dc28ffd1a17010da12
# Parent  b3b1f4184ae4a3dcbb3fe68fc9148fe06ae0c1ac
simplifief 'method_setup' command;

diff -r b3b1f4184ae4 -r 4c2514625873 NEWS
--- a/NEWS	Mon Mar 16 17:48:02 2009 +0100
+++ b/NEWS	Mon Mar 16 17:51:07 2009 +0100
@@ -603,7 +603,10 @@
 or later]
 
 * Simplified ML attribute and method setup, cf. functions Attrib.setup
-and Method.setup, as well as commands 'attribute_setup'.
+and Method.setup, as well as commands 'attribute_setup' and
+'method_setup'.  INCOMPATIBILITY for 'method_setup', need to simplify
+existing code accordingly, or use plain 'setup' together with old
+Method.add_method.
 
 * Simplified ML oracle interface Thm.add_oracle promotes 'a -> cterm
 to 'a -> thm, while results are always tagged with an authentic oracle
diff -r b3b1f4184ae4 -r 4c2514625873 doc-src/IsarRef/Thy/Proof.thy
--- a/doc-src/IsarRef/Thy/Proof.thy	Mon Mar 16 17:48:02 2009 +0100
+++ b/doc-src/IsarRef/Thy/Proof.thy	Mon Mar 16 17:51:07 2009 +0100
@@ -886,32 +886,33 @@
 
   \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.
+  "text"} has to be an ML expression of type
+  @{ML_type "(Proof.context -> Proof.method) context_parser"}, cf.\
+  basic parsers defined in structure @{ML_struct Args} and @{ML_struct
+  Attrib}.  There are also combinators like @{ML METHOD} and @{ML
+  SIMPLE_METHOD} to turn certain tactic forms into official proof
+  methods; the primed versions refer to tactics with explicit goal
+  addressing.
 
-%FIXME proper antiquotations
-{\footnotesize
-\begin{verbatim}
- Method.no_args (METHOD (fn facts => foobar_tac))
- Method.thms_args (fn thms => METHOD (fn facts => foobar_tac))
- Method.ctxt_args (fn ctxt => METHOD (fn facts => foobar_tac))
- Method.thms_ctxt_args (fn thms => fn ctxt => 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.
+  Here are some example method definitions:
 
   \end{description}
 *}
 
+    method_setup my_method1 = {*
+      Scan.succeed (K (SIMPLE_METHOD' (fn i: int => no_tac)))
+    *}  "my first method (without any arguments)"
+
+    method_setup my_method2 = {*
+      Scan.succeed (fn ctxt: Proof.context =>
+        SIMPLE_METHOD' (fn i: int => no_tac))
+    *}  "my second method (with context)"
+
+    method_setup my_method3 = {*
+      Attrib.thms >> (fn thms: thm list => fn ctxt: Proof.context =>
+        SIMPLE_METHOD' (fn i: int => no_tac))
+    *}  "my third method (with theorem arguments and context)"
+
 
 section {* Generalized elimination \label{sec:obtain} *}
 
@@ -1041,7 +1042,7 @@
 
   \begin{matharray}{rcl}
     @{command "also"}@{text "\<^sub>0"} & \equiv & @{command "note"}~@{text "calculation = this"} \\
-    @{command "also"}@{text "\<^sub>n\<^sub>+\<^sub>1"} & \equiv & @{command "note"}~@{text "calculation = trans [OF calculation this]"} \\[0.5ex]
+    @{command "also"}@{text "\<^sub>n+1"} & \equiv & @{command "note"}~@{text "calculation = trans [OF calculation this]"} \\[0.5ex]
     @{command "finally"} & \equiv & @{command "also"}~@{command "from"}~@{text calculation} \\[0.5ex]
     @{command "moreover"} & \equiv & @{command "note"}~@{text "calculation = calculation this"} \\
     @{command "ultimately"} & \equiv & @{command "moreover"}~@{command "from"}~@{text calculation} \\