# HG changeset patch
# User wenzelm
# Date 955575921 -7200
# Node ID 734a0206e9f90da4590cb80f59ee1f00f3300b11
# Parent  48786b52c8d8e46060a7938ad9568c0791463a4a
added 'insert' method;

diff -r 48786b52c8d8 -r 734a0206e9f9 doc-src/IsarRef/refcard.tex
--- 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}