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