253 by \(tac@1\); |
253 by \(tac@1\); |
254 \(\vdots\) |
254 \(\vdots\) |
255 qed_spec_mp "\(name\)"; |
255 qed_spec_mp "\(name\)"; |
256 \end{ttbox} |
256 \end{ttbox} |
257 The operation performed by \texttt{qed_spec_mp} is also performed by the Isar |
257 The operation performed by \texttt{qed_spec_mp} is also performed by the Isar |
258 attribute ``$rule_format$'', see also \S\ref{sec:rule-format}. Thus the |
258 attribute ``$rule_format$'', see also \S\ref{sec:object-logic}. Thus the |
259 corresponding Isar text may look like this: |
259 corresponding Isar text may look like this: |
260 \begin{matharray}{l} |
260 \begin{matharray}{l} |
261 \LEMMA{name~[rule_format]}{\texttt"{\phi}\texttt"} \\ |
261 \LEMMA{name~[rule_format]}{\texttt"{\phi}\texttt"} \\ |
262 \quad \APPLY{meth@1} \\ |
262 \quad \APPLY{meth@1} \\ |
263 \qquad \vdots \\ |
263 \qquad \vdots \\ |
308 $drule_tac$, $frule_tac$ (see \S\ref{sec:tactics}) would be sufficient to |
308 $drule_tac$, $frule_tac$ (see \S\ref{sec:tactics}) would be sufficient to |
309 cover the four modes, either with or without instantiation, and either with |
309 cover the four modes, either with or without instantiation, and either with |
310 single or multiple arguments. Although it is more convenient in most cases to |
310 single or multiple arguments. Although it is more convenient in most cases to |
311 use the plain $rule$ method (see \S\ref{sec:pure-meth-att}), or any of its |
311 use the plain $rule$ method (see \S\ref{sec:pure-meth-att}), or any of its |
312 ``improper'' variants $erule$, $drule$, $frule$ (see |
312 ``improper'' variants $erule$, $drule$, $frule$ (see |
313 \S\ref{sec:misc-methods}). Note that explicit goal addressing is only |
313 \S\ref{sec:misc-meth-att}). Note that explicit goal addressing is only |
314 supported by the actual $rule_tac$ version. |
314 supported by the actual $rule_tac$ version. |
315 |
315 |
316 With this in mind, plain resolution tactics may be ported as follows. |
316 With this in mind, plain resolution tactics may be ported as follows. |
317 \begin{matharray}{lll} |
317 \begin{matharray}{lll} |
318 \texttt{rtac}~a~1 & & rule~a \\ |
318 \texttt{rtac}~a~1 & & rule~a \\ |