author wenzelm Mon, 14 Aug 2000 18:45:31 +0200 changeset 9603 816917b6c2de parent 9602 900df8e67fcf child 9604 abe51fcb2222
updated; tuned;
--- a/doc-src/IsarRef/refcard.tex	Mon Aug 14 18:45:16 2000 +0200
+++ b/doc-src/IsarRef/refcard.tex	Mon Aug 14 18:45:31 2000 +0200
@@ -80,9 +80,6 @@
\isarkeyword{term}~t & \text{print term} \\
\isarkeyword{prop}~\phi & \text{print meta-level proposition} \\
\isarkeyword{typ}~\tau & \text{print meta-level type} \\
-  \isarkeyword{print_facts} & \text{print named facts} \\
-  \isarkeyword{print_binds} & \text{print term abbreviations} \\
-  \isarkeyword{print_cases} & \text{print named cases} \\
\end{matharray}

@@ -106,9 +103,9 @@
$unfold~\vec a$ & \text{definitions} \\[2ex]

\multicolumn{2}{l}{\textbf{Automated proof tools (inserting facts, or even prems!)}} \\[0.5ex]
-  $simp$ & Simplifier (+ Splitter) \\
+  $simp$, $simp_all$ & Simplifier (+ Splitter) \\
$blast$, $fast$ & Classical Reasoner \\
-  $force$, $auto$ & Simplifier + Classical Reasoner \\
+  $auto$, $force$ & Simplifier + Classical Reasoner \\
$arith$ & Arithmetic procedure \\
\end{tabular}

@@ -148,15 +145,14 @@
\subsection{Methods}

\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 \\
+  $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 \\
$case_tac~t$ & exhaustion (datatypes) \\
$induct_tac~\vec x$ & induction (datatypes) \\
+  $tactic~text$ & method from ML tactic \\
\end{tabular}