--- a/doc-src/IsarRef/refcard.tex Mon Mar 20 18:25:35 2000 +0100
+++ b/doc-src/IsarRef/refcard.tex Mon Mar 20 18:42:50 2000 +0100
@@ -144,13 +144,16 @@
\begin{tabular}{ll}
$tactic~text$ & method from ML tactic \\
+ $res_inst_tac~insts$ & resolution with instantiation \\
+ $eres_inst_tac~insts$ & elim-resolution with instantiation \\
+ $dres_inst_tac~insts$ & destruct-resolution with instantiation \\
+ $forw_inst_tac~insts$ & forward-resolution with instantiation \\
+ $subgoal_tac~\phi$ & insert new claim \\
+ $case_tac~t$ & datatype exhaustion \\
+ $induct_tac~xs$ & datatype induction \\
\end{tabular}
-
-
-
-
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "isar-ref"