diff -r 79e1e99e0a2a -r 6ac8c55c657e doc-src/IsarRef/Thy/ML_Tactic.thy
--- a/doc-src/IsarRef/Thy/ML_Tactic.thy	Mon May 02 20:14:19 2011 +0200
+++ b/doc-src/IsarRef/Thy/ML_Tactic.thy	Mon May 02 20:34:34 2011 +0200
@@ -51,11 +51,10 @@
   \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 @{method rule} method (see
-  \secref{sec:pure-meth-att}), or any of its ``improper'' variants
-  @{method erule}, @{method drule}, @{method frule} (see
-  \secref{sec:misc-meth-att}).  Note that explicit goal addressing is
-  only supported by the actual @{method rule_tac} version.
+  use the plain @{method_ref (Pure) rule} method, or any of its
+  ``improper'' variants @{method erule}, @{method drule}, @{method
+  frule}.  Note that explicit goal addressing is only supported by the
+  actual @{method rule_tac} version.
 
   With this in mind, plain resolution tactics correspond to Isar
   methods as follows.