# HG changeset patch
# User wenzelm
# Date 953574170 -3600
# Node ID ed6962a0763f9c5acde4b12758f1f0b08242f647
# Parent  4656e8312ba9c0e1438a521e75aacc91b732b90e
tactic emulation;

diff -r 4656e8312ba9 -r ed6962a0763f doc-src/IsarRef/refcard.tex
--- 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"