--- a/doc-src/IsarRef/Thy/document/ML_Tactic.tex Mon May 02 20:14:19 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/ML_Tactic.tex Mon May 02 20:34:34 2011 +0200
@@ -70,11 +70,9 @@
\secref{sec:tactics}) would be sufficient to cover the four modes,
either with or without instantiation, and either with single or
multiple arguments. Although it is more convenient in most cases to
- use the plain \hyperlink{method.rule}{\mbox{\isa{rule}}} method (see
- \secref{sec:pure-meth-att}), or any of its ``improper'' variants
- \hyperlink{method.erule}{\mbox{\isa{erule}}}, \hyperlink{method.drule}{\mbox{\isa{drule}}}, \hyperlink{method.frule}{\mbox{\isa{frule}}} (see
- \secref{sec:misc-meth-att}). Note that explicit goal addressing is
- only supported by the actual \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}tac}}} version.
+ use the plain \indexref{Pure}{method}{rule}\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}} method, or any of its
+ ``improper'' variants \hyperlink{method.erule}{\mbox{\isa{erule}}}, \hyperlink{method.drule}{\mbox{\isa{drule}}}, \hyperlink{method.frule}{\mbox{\isa{frule}}}. Note that explicit goal addressing is only supported by the
+ actual \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isaliteral{5F}{\isacharunderscore}}tac}}} version.
With this in mind, plain resolution tactics correspond to Isar
methods as follows.