# HG changeset patch
# User wenzelm
# Date 1288731561 -3600
# Node ID a0698ec82e6ee6d58ec66a53d0be799357afdb87
# Parent  de842e206db20cd6158f6c0aee6a0236b9a80c57
more on naming tactics;

diff -r de842e206db2 -r a0698ec82e6e doc-src/IsarImplementation/Thy/ML.thy
--- a/doc-src/IsarImplementation/Thy/ML.thy	Tue Nov 02 21:24:07 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Tue Nov 02 21:59:21 2010 +0100
@@ -262,6 +262,22 @@
   @{ML_text lhs} (not @{ML_text lhs_tm}).  Or a term that is known
   to be a variable can be called @{ML_text v} or @{ML_text x}.
 
+  \item Tactics (\secref{sec:tactics}) are sufficiently important to
+  have specific naming conventions.  The name of a basic tactic
+  definition always has a @{ML_text "_tac"} suffix, the subgoal index
+  (if applicable) is always called @{ML_text i}, and the goal state
+  (if made explicit) is usually called @{ML_text st} instead of the
+  somewhat misleading @{ML_text thm}.  Any other arguments are given
+  before the latter two, and the general context is given first.
+  Example:
+
+  \begin{verbatim}
+  fun my_tac ctxt arg1 arg2 i st = ...
+  \end{verbatim}
+
+  Note that the goal state @{ML_text st} above is rarely made
+  explicit, if tactic combinators (tacticals) are used as usual.
+
   \end{itemize}
 *}
 
diff -r de842e206db2 -r a0698ec82e6e doc-src/IsarImplementation/Thy/document/ML.tex
--- a/doc-src/IsarImplementation/Thy/document/ML.tex	Tue Nov 02 21:24:07 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Tue Nov 02 21:59:21 2010 +0100
@@ -281,6 +281,22 @@
   \verb|lhs| (not \verb|lhs_tm|).  Or a term that is known
   to be a variable can be called \verb|v| or \verb|x|.
 
+  \item Tactics (\secref{sec:tactics}) are sufficiently important to
+  have specific naming conventions.  The name of a basic tactic
+  definition always has a \verb|_tac| suffix, the subgoal index
+  (if applicable) is always called \verb|i|, and the goal state
+  (if made explicit) is usually called \verb|st| instead of the
+  somewhat misleading \verb|thm|.  Any other arguments are given
+  before the latter two, and the general context is given first.
+  Example:
+
+  \begin{verbatim}
+  fun my_tac ctxt arg1 arg2 i st = ...
+  \end{verbatim}
+
+  Note that the goal state \verb|st| above is rarely made
+  explicit, if tactic combinators (tacticals) are used as usual.
+
   \end{itemize}%
 \end{isamarkuptext}%
 \isamarkuptrue%