author wenzelm Wed, 07 Aug 2002 17:36:05 +0200 changeset 13472 2529a53514e6 parent 13471 aed3aef2a0ca child 13473 194e8d2cbe0f
section on "Rule declarations and methods";
--- a/doc-src/IsarRef/refcard.tex	Wed Aug 07 16:50:08 2002 +0200
+++ b/doc-src/IsarRef/refcard.tex	Wed Aug 07 17:36:05 2002 +0200
@@ -107,8 +107,8 @@

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

+\section{Rule declarations and methods}
+
+\begin{tabular}{l|lllll}
+                          & $rule$   & $rules$  & $blast$ etc. & $simp$ etc. & $auto$ etc. \\
+  \hline
+  $elim!$ $intro!$ (Pure) & $\times$ & $\times$ \\
+  $elim$ $intro$ (Pure)   & $\times$ & $\times$ \\
+  $elim!$ $intro!$        & $\times$ &          & $\times$     &             & $\times$ \\
+  $elim$ $intro$          & $\times$ &          & $\times$     &             & $\times$ \\
+  $iff$                   & $\times$ &          & $\times$     & $\times$    & $\times$ \\
+  $iff?$                  & $\times$ \\
+  $elim?$ $intro?$        & $\times$ \\
+  $simp$                  &          &          &              & $\times$    & $\times$ \\
+  $cong$                  &          &          &              & $\times$    & $\times$ \\
+  $split$                 &          &          &              & $\times$    & $\times$ \\
+\end{tabular}
+
+
\section{Emulating tactic scripts}

\subsection{Commands}