# HG changeset patch
# User wenzelm
# Date 966501103 -7200
# Node ID 6eafc4d2ed851304b1a24ec1481b0de53bc4e6bc
# Parent  8ca1fc75230e726da02dd1f8f448e82f7b75d8fd
updated;

diff -r 8ca1fc75230e -r 6eafc4d2ed85 doc-src/IsarRef/refcard.tex
--- a/doc-src/IsarRef/refcard.tex	Thu Aug 17 10:31:10 2000 +0200
+++ b/doc-src/IsarRef/refcard.tex	Thu Aug 17 10:31:43 2000 +0200
@@ -116,7 +116,8 @@
   \multicolumn{2}{l}{\textbf{Manipulate rules}} \\[0.5ex]
   $OF~\vec a$ & apply rule to facts (skipping ``$_$'') \\
   $of~\vec t$ & apply rule to terms (skipping ``$_$'') \\
-  $RS~b$ & resolve fact with rule \\
+  $THEN~b$ & resolve fact with rule \\
+  $symmetric$ & apply symmetry of equality \\
   $standard$ & put into standard result form \\
   $rulify$ & put into object-rule form \\
   $elimify$ & put destruction rule into elimination form \\[1ex]
@@ -137,26 +138,33 @@
 \begin{tabular}{ll}
   $\isarkeyword{apply}~(m)$ & apply proof method at initial position \\
   $\isarkeyword{apply_end}~(m)$ & apply proof method near terminal position \\
+  $\isarkeyword{done}$ & complete proof \\
   $\isarkeyword{defer}~n$ & move subgoal to end \\
   $\isarkeyword{prefer}~n$ & move subgoal to beginning \\
   $\isarkeyword{back}$ & backtrack last command \\
+  $\isarkeyword{declare}$ & declare rules in current theory \\
 \end{tabular}
 
 \subsection{Methods}
 
 \begin{tabular}{ll}
-  $rule_tac~insts$ & resolution with instantiation \\
-  $erule_tac~insts$ & elim-resolution with instantiation \\
-  $drule_tac~insts$ & destruct-resolution with instantiation \\
-  $frule_tac~insts$ & forward-resolution with instantiation \\
-  $subgoal_tac~\phi$ & insert new claims \\
+  $rule_tac~insts$ & resolution (with instantiation) \\
+  $erule_tac~insts$ & elim-resolution (with instantiation) \\
+  $drule_tac~insts$ & destruct-resolution (with instantiation) \\
+  $frule_tac~insts$ & forward-resolution (with instantiation) \\
+  $cut_tac~insts$ & insert facts (with instantiation) \\
+  $thin_tac~\phi$ & delete assumptions \\
+  $subgoal_tac~\phi$ & new claims \\
+  $rename_tac~\vec x$ & rename suffix of goal parameters \\
+  $rotate_tac~n$ & rotate assumptions of goal \\
+  $tactic~text$ & arbitrary ML tactic \\
   $case_tac~t$ & exhaustion (datatypes) \\
   $induct_tac~\vec x$ & induction (datatypes) \\
-  $tactic~text$ & method from ML tactic \\
+  $ind_cases~t$ & exhaustion + simplification (inductive sets) \\
 \end{tabular}
 
 
-%%% Local Variables: 
+%%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "isar-ref"
-%%% End: 
+%%% End: