author wenzelm Thu, 17 Aug 2000 10:31:43 +0200 changeset 9615 6eafc4d2ed85 parent 9614 8ca1fc75230e child 9616 b80ea2b32f8e
updated;
--- a/doc-src/IsarRef/refcard.tex	Thu Aug 17 10:31:10 2000 +0200
+++ b/doc-src/IsarRef/refcard.tex	Thu Aug 17 10:31:43 2000 +0200
@@ -116,7 +116,8 @@
\multicolumn{2}{l}{\textbf{Manipulate rules}} \\[0.5ex]
$OF~\vec a$ & apply rule to facts (skipping $_$'') \\
$of~\vec t$ & apply rule to terms (skipping $_$'') \\
-  $RS~b$ & resolve fact with rule \\
+  $THEN~b$ & resolve fact with rule \\
+  $symmetric$ & apply symmetry of equality \\
$standard$ & put into standard result form \\
$rulify$ & put into object-rule form \\
$elimify$ & put destruction rule into elimination form \\[1ex]
@@ -137,26 +138,33 @@
\begin{tabular}{ll}
$\isarkeyword{apply}~(m)$ & apply proof method at initial position \\
$\isarkeyword{apply_end}~(m)$ & apply proof method near terminal position \\
+  $\isarkeyword{done}$ & complete proof \\
$\isarkeyword{defer}~n$ & move subgoal to end \\
$\isarkeyword{prefer}~n$ & move subgoal to beginning \\
$\isarkeyword{back}$ & backtrack last command \\
+  $\isarkeyword{declare}$ & declare rules in current theory \\
\end{tabular}

\subsection{Methods}

\begin{tabular}{ll}
-  $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 \\
+  $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) \\
+  $cut_tac~insts$ & insert facts (with instantiation) \\
+  $thin_tac~\phi$ & delete assumptions \\
+  $subgoal_tac~\phi$ & new claims \\
+  $rename_tac~\vec x$ & rename suffix of goal parameters \\
+  $rotate_tac~n$ & rotate assumptions of goal \\
+  $tactic~text$ & arbitrary ML tactic \\
$case_tac~t$ & exhaustion (datatypes) \\
$induct_tac~\vec x$ & induction (datatypes) \\
-  $tactic~text$ & method from ML tactic \\
+  $ind_cases~t$ & exhaustion + simplification (inductive sets) \\
\end{tabular}

-%%% Local Variables:
+%%% Local Variables:
%%% mode: latex
%%% TeX-master: "isar-ref"
-%%% End:
+%%% End: