diff -r 79e1e99e0a2a -r 6ac8c55c657e doc-src/IsarRef/Thy/Framework.thy
--- a/doc-src/IsarRef/Thy/Framework.thy	Mon May 02 20:14:19 2011 +0200
+++ b/doc-src/IsarRef/Thy/Framework.thy	Mon May 02 20:34:34 2011 +0200
@@ -521,23 +521,23 @@
   "then"} or @{command using}, and then operate on the goal state.
   Some basic methods are predefined: ``@{method "-"}'' leaves the goal
   unchanged, ``@{method this}'' applies the facts as rules to the
-  goal, ``@{method "rule"}'' applies the facts to another rule and the
-  result to the goal (both ``@{method this}'' and ``@{method rule}''
+  goal, ``@{method (Pure) "rule"}'' applies the facts to another rule and the
+  result to the goal (both ``@{method this}'' and ``@{method (Pure) rule}''
   refer to @{inference resolution} of
   \secref{sec:framework-resolution}).  The secondary arguments to
-  ``@{method rule}'' may be specified explicitly as in ``@{text "(rule
+  ``@{method (Pure) rule}'' may be specified explicitly as in ``@{text "(rule
   a)"}'', or picked from the context.  In the latter case, the system
   first tries rules declared as @{attribute (Pure) elim} or
   @{attribute (Pure) dest}, followed by those declared as @{attribute
   (Pure) intro}.
 
-  The default method for @{command proof} is ``@{method rule}''
+  The default method for @{command proof} is ``@{method (Pure) rule}''
   (arguments picked from the context), for @{command qed} it is
   ``@{method "-"}''.  Further abbreviations for terminal proof steps
   are ``@{command "by"}~@{text "method\<^sub>1 method\<^sub>2"}'' for
   ``@{command proof}~@{text "method\<^sub>1"}~@{command qed}~@{text
   "method\<^sub>2"}'', and ``@{command ".."}'' for ``@{command
-  "by"}~@{method rule}, and ``@{command "."}'' for ``@{command
+  "by"}~@{method (Pure) rule}, and ``@{command "."}'' for ``@{command
   "by"}~@{method this}''.  The @{command unfolding} element operates
   directly on the current facts and goal by applying equalities.