# HG changeset patch
# User wenzelm
# Date 977937954 -3600
# Node ID 8256cfec20408a79398c5bbe0b74a20765ce9dcd
# Parent  ec19f5902ef51245c96c1c03df31c5d24163278a
ares_tac, [edf]atac;

diff -r ec19f5902ef5 -r 8256cfec2040 doc-src/IsarRef/conversion.tex
--- a/doc-src/IsarRef/conversion.tex	Sat Dec 23 22:53:27 2000 +0100
+++ b/doc-src/IsarRef/conversion.tex	Wed Dec 27 18:25:54 2000 +0100
@@ -329,6 +329,15 @@
 order of subgoals with $\isarkeyword{defer}$ or $\isarkeyword{prefer}$ (see
 \S\ref{sec:tactic-commands}).
 
+\medskip Some further (less frequently used) combinations of basic resolution
+tactics may be expressed as follows.
+\begin{matharray}{lll}
+  \texttt{ares_tac}~[a@1, \dots]~1 & & assumption~|~rule~a@1~\dots \\
+  \texttt{eatac}~a~n~1 & & erule~(n)~a \\
+  \texttt{datac}~a~n~1 & & drule~(n)~a \\
+  \texttt{fatac}~a~n~1 & & frule~(n)~a \\
+\end{matharray}
+
 
 \subsubsection{Simplifier tactics}