diff -r aed3aef2a0ca -r 2529a53514e6 doc-src/IsarRef/refcard.tex
--- a/doc-src/IsarRef/refcard.tex	Wed Aug 07 16:50:08 2002 +0200
+++ b/doc-src/IsarRef/refcard.tex	Wed Aug 07 17:36:05 2002 +0200
@@ -107,8 +107,8 @@
 
   \multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts, or even prems!)}} \\[0.5ex]
   $rules$ & \Text{intuitionistic proof search} \\
+  $blast$, $fast$ & Classical Reasoner \\
   $simp$, $simp_all$ & Simplifier (+ Splitter) \\
-  $blast$, $fast$ & Classical Reasoner \\
   $auto$, $force$ & Simplifier + Classical Reasoner \\
   $arith$ & Arithmetic procedure \\
 \end{tabular}
@@ -135,6 +135,24 @@
 \end{tabular}
 
 
+\section{Rule declarations and methods}
+
+\begin{tabular}{l|lllll}
+                          & $rule$   & $rules$  & $blast$ etc. & $simp$ etc. & $auto$ etc. \\
+  \hline
+  $elim!$ $intro!$ (Pure) & $\times$ & $\times$ \\
+  $elim$ $intro$ (Pure)   & $\times$ & $\times$ \\
+  $elim!$ $intro!$        & $\times$ &          & $\times$     &             & $\times$ \\
+  $elim$ $intro$          & $\times$ &          & $\times$     &             & $\times$ \\
+  $iff$                   & $\times$ &          & $\times$     & $\times$    & $\times$ \\
+  $iff?$                  & $\times$ \\
+  $elim?$ $intro?$        & $\times$ \\
+  $simp$                  &          &          &              & $\times$    & $\times$ \\
+  $cong$                  &          &          &              & $\times$    & $\times$ \\
+  $split$                 &          &          &              & $\times$    & $\times$ \\
+\end{tabular}
+
+
 \section{Emulating tactic scripts}
 
 \subsection{Commands}