--- a/doc-src/IsarRef/refcard.tex Wed Apr 12 23:45:01 2000 +0200
+++ b/doc-src/IsarRef/refcard.tex Wed Apr 12 23:45:21 2000 +0200
@@ -150,13 +150,14 @@
\begin{tabular}{ll}
$tactic~text$ & method from ML tactic \\
+ $insert~\vec a$ & insert theorems (ignoring current facts) \\
$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~\vec x$ & datatype induction \\
+ $case_tac~t$ & exhaustion (datatypes) \\
+ $induct_tac~\vec x$ & induction (datatypes) \\
\end{tabular}