# HG changeset patch
# User wenzelm
# Date 962311005 -7200
# Node ID 7a1a856f0571cd9771eb9b52eb1e32e6569b781e
# Parent  0ab3c81e94253f2e848af6d349def79a89f5f490
facts: support multiple lists of arguments;
method_setup command;

diff -r 0ab3c81e9425 -r 7a1a856f0571 doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Thu Jun 29 22:35:45 2000 +0200
+++ b/doc-src/IsarRef/pure.tex	Thu Jun 29 22:36:45 2000 +0200
@@ -297,7 +297,7 @@
 \begin{rail}
   'axioms' (axmdecl prop comment? +)
   ;
-  ('theorems' | 'lemmas') thmdef? thmrefs
+  ('theorems' | 'lemmas') (thmdef? thmrefs comment? + 'and')
   ;
 \end{rail}
 
@@ -364,17 +364,22 @@
 
 \indexisarcmd{use}\indexisarcmd{ML}\indexisarcmd{ML-command}
 \indexisarcmd{ML-setup}\indexisarcmd{setup}
+\indexisarcmd{method-setup}
 \begin{matharray}{rcl}
   \isarcmd{use} & : & \isartrans{\cdot}{\cdot} \\
   \isarcmd{ML} & : & \isartrans{\cdot}{\cdot} \\
   \isarcmd{ML_command} & : & \isartrans{\cdot}{\cdot} \\
   \isarcmd{ML_setup} & : & \isartrans{theory}{theory} \\
   \isarcmd{setup} & : & \isartrans{theory}{theory} \\
+  \isarcmd{method_setup} & : & \isartrans{theory}{theory} \\
 \end{matharray}
 
 \railalias{MLsetup}{ML\_setup}
 \railterm{MLsetup}
 
+\railalias{methodsetup}{method\_setup}
+\railterm{methodsetup}
+
 \railalias{MLcommand}{ML\_command}
 \railterm{MLcommand}
 
@@ -383,6 +388,8 @@
   ;
   ('ML' | MLcommand | MLsetup | 'setup') text
   ;
+  methodsetup name '=' text text comment?
+  ;
 \end{rail}
 
 \begin{descr}
@@ -406,6 +413,27 @@
   \texttt{(theory~->~theory)~list}.  The $\isarkeyword{setup}$ command is the
   canonical way to initialize any object-logic specific tools and packages
   written in ML.
+  
+\item [$\isarkeyword{method_setup}~name = text~description$] defines a proof
+  method in the current theory.  The given $text$ has to be an ML expression
+  of type \texttt{Args.src -> Proof.context -> Proof.method}.  Parsing
+  concrete method syntax from \texttt{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.
+
+{\footnotesize
+\begin{verbatim}
+Method.no_args (Method.METHOD (fn facts => foobar_tac))
+Method.thms_args (fn thms => (Method.METHOD (fn facts => foobar_tac)))
+\end{verbatim}
+}
+
+Note that mere tactic emulations may ignore the \texttt{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 \texttt{Method.multi_resolves}), while
+automatic ones just insert the facts using \texttt{Method.insert_tac} before
+applying the main tactic.
 \end{descr}
 
 
@@ -600,11 +628,11 @@
 $\THEN$ (and variants).  Note that the special theorem name
 $this$\indexisarthm{this} refers to the most recently established facts.
 \begin{rail}
-  'note' thmdef? thmrefs comment?
+  'note' (thmdef? thmrefs comment? + 'and')
   ;
   'then' comment?
   ;
-  ('from' | 'with') thmrefs comment?
+  ('from' | 'with') (thmrefs comment? + 'and')
   ;
 \end{rail}
 
@@ -1242,13 +1270,6 @@
   result in utter confusion.
 \end{warn}
 
-%FIXME remove
-% \begin{descr}
-% \item [$\isarkeyword{undo}$] revokes the latest state-transforming command.
-% \item [$\isarkeyword{redo}$] undos the latest $\isarkeyword{undo}$.
-% \item [$\isarkeyword{kill}$] aborts the current history level.
-% \end{descr}
-
 
 \subsection{System operations}