322 \end{rail} |
322 \end{rail} |
323 |
323 |
324 \begin{descr} |
324 \begin{descr} |
325 |
325 |
326 \item [\hyperlink{method.rule-tac}{\mbox{\isa{rule{\isacharunderscore}tac}}} etc.] do resolution of rules with explicit |
326 \item [\hyperlink{method.rule-tac}{\mbox{\isa{rule{\isacharunderscore}tac}}} etc.] do resolution of rules with explicit |
327 instantiation. This works the same way as the ML tactics \verb|res_inst_tac| etc. (see \cite[\S3]{isabelle-ref}). |
327 instantiation. This works the same way as the ML tactics \verb|Tactic.res_inst_tac| etc. (see \cite[\S3]{isabelle-ref}) |
328 |
328 |
329 Multiple rules may be only given if there is no instantiation; then |
329 Multiple rules may be only given if there is no instantiation; then |
330 \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isacharunderscore}tac}}} is the same as \verb|resolve_tac| in ML (see |
330 \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isacharunderscore}tac}}} is the same as \verb|resolve_tac| in ML (see |
331 \cite[\S3]{isabelle-ref}). |
331 \cite[\S3]{isabelle-ref}). |
332 |
332 |
333 \item [\hyperlink{method.cut-tac}{\mbox{\isa{cut{\isacharunderscore}tac}}}] inserts facts into the proof state as |
333 \item [\hyperlink{method.cut-tac}{\mbox{\isa{cut{\isacharunderscore}tac}}}] inserts facts into the proof state as |
334 assumption of a subgoal, see also \verb|cut_facts_tac| in |
334 assumption of a subgoal, see also \verb|Tactic.cut_facts_tac| in |
335 \cite[\S3]{isabelle-ref}. Note that the scope of schematic |
335 \cite[\S3]{isabelle-ref}. Note that the scope of schematic |
336 variables is spread over the main goal statement. Instantiations |
336 variables is spread over the main goal statement. Instantiations |
337 may be given as well, see also ML tactic \verb|cut_inst_tac| in |
337 may be given as well, see also ML tactic \verb|Tactic.cut_inst_tac| |
338 \cite[\S3]{isabelle-ref}. |
338 in \cite[\S3]{isabelle-ref}. |
339 |
339 |
340 \item [\hyperlink{method.thin-tac}{\mbox{\isa{thin{\isacharunderscore}tac}}}~\isa{{\isasymphi}}] deletes the specified |
340 \item [\hyperlink{method.thin-tac}{\mbox{\isa{thin{\isacharunderscore}tac}}}~\isa{{\isasymphi}}] deletes the specified |
341 assumption from a subgoal; note that \isa{{\isasymphi}} may contain schematic |
341 assumption from a subgoal; note that \isa{{\isasymphi}} may contain schematic |
342 variables. See also \verb|thin_tac| in \cite[\S3]{isabelle-ref}. |
342 variables. See also \verb|Tactic.thin_tac| in |
|
343 \cite[\S3]{isabelle-ref}. |
343 |
344 |
344 \item [\hyperlink{method.subgoal-tac}{\mbox{\isa{subgoal{\isacharunderscore}tac}}}~\isa{{\isasymphi}}] adds \isa{{\isasymphi}} as an |
345 \item [\hyperlink{method.subgoal-tac}{\mbox{\isa{subgoal{\isacharunderscore}tac}}}~\isa{{\isasymphi}}] adds \isa{{\isasymphi}} as an |
345 assumption to a subgoal. See also \verb|subgoal_tac| and \verb|subgoals_tac| in \cite[\S3]{isabelle-ref}. |
346 assumption to a subgoal. See also \verb|Tactic.subgoal_tac| and \verb|Tactic.subgoals_tac| in \cite[\S3]{isabelle-ref}. |
346 |
347 |
347 \item [\hyperlink{method.rename-tac}{\mbox{\isa{rename{\isacharunderscore}tac}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isachardoublequote}}] renames |
348 \item [\hyperlink{method.rename-tac}{\mbox{\isa{rename{\isacharunderscore}tac}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isachardoublequote}}] renames |
348 parameters of a goal according to the list \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub n{\isachardoublequote}}, which refers to the \emph{suffix} of variables. |
349 parameters of a goal according to the list \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub n{\isachardoublequote}}, which refers to the \emph{suffix} of variables. |
349 |
350 |
350 \item [\hyperlink{method.rotate-tac}{\mbox{\isa{rotate{\isacharunderscore}tac}}}~\isa{n}] rotates the assumptions of a |
351 \item [\hyperlink{method.rotate-tac}{\mbox{\isa{rotate{\isacharunderscore}tac}}}~\isa{n}] rotates the assumptions of a |