--- a/doc-src/IsarRef/refcard.tex Fri Aug 29 15:19:02 2003 +0200
+++ b/doc-src/IsarRef/refcard.tex Fri Aug 29 15:40:11 2003 +0200
@@ -118,8 +118,9 @@
\begin{tabular}{ll}
\multicolumn{2}{l}{\textbf{Operations}} \\[0.5ex]
- $OF~\vec a$ & rule applied to facts (skipping ``$_$'') \\
- $of~\vec t$ & rule applied to terms (skipping ``$_$'') \\
+ $OF~\vec a$ & rule resolved with facts (skipping ``$_$'') \\
+ $of~\vec t$ & rule instantiated with terms (skipping ``$_$'') \\
+ $where~\vec x = \vec t$ & rule instantiated with terms, by variable name \\
$symmetric$ & resolution with symmetry rule \\
$THEN~b$ & resolution with another rule \\
$rule_format$ & result put into standard rule format \\