equal
deleted
inserted
replaced
64 equalities ($\equiv$). More general equivalences are handled by the |
64 equalities ($\equiv$). More general equivalences are handled by the |
65 simplifier, provided that it is set up appropriately for your logic |
65 simplifier, provided that it is set up appropriately for your logic |
66 (see Chapter~\ref{chap:simplification}). |
66 (see Chapter~\ref{chap:simplification}). |
67 \end{warn} |
67 \end{warn} |
68 |
68 |
69 \subsection{Theorems useful with tactics} |
|
70 \index{theorems!of pure theory} |
|
71 \begin{ttbox} |
|
72 asm_rl: thm |
|
73 \end{ttbox} |
|
74 \begin{ttdescription} |
|
75 \item[\tdx{asm_rl}] |
|
76 is $\psi\Imp\psi$. Under elim-resolution it does proof by assumption, and |
|
77 \hbox{\tt eresolve_tac (asm_rl::{\it thms}) {\it i}} is equivalent to |
|
78 \begin{ttbox} |
|
79 assume_tac {\it i} ORELSE eresolve_tac {\it thms} {\it i} |
|
80 \end{ttbox} |
|
81 |
|
82 \end{ttdescription} |
|
83 |
|
84 |
|
85 \section{Obscure tactics} |
|
86 |
69 |
87 \subsection{Composition: resolution without lifting} |
70 \subsection{Composition: resolution without lifting} |
88 \index{tactics!for composition} |
71 \index{tactics!for composition} |
89 \begin{ttbox} |
72 \begin{ttbox} |
90 compose_tac: (bool * thm * int) -> int -> tactic |
73 compose_tac: (bool * thm * int) -> int -> tactic |