# HG changeset patch
# User wenzelm
# Date 1304361274 -7200
# Node ID 6ac8c55c657ede22016db59a59846019a17ca731
# Parent  79e1e99e0a2a8605b0e77130ca357a29c5690d8a
eliminated some duplicate "def" positions;

diff -r 79e1e99e0a2a -r 6ac8c55c657e doc-src/IsarRef/Thy/Document_Preparation.thy
--- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Mon May 02 20:14:19 2011 +0200
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Mon May 02 20:34:34 2011 +0200
@@ -399,7 +399,7 @@
   not under direct control of the author, it may even fluctuate a bit
   as the underlying theory is changed later on.
 
-  In contrast, @{antiquotation_option_def source}~@{text "= true"}
+  In contrast, @{antiquotation_option source}~@{text "= true"}
   admits direct printing of the given source text, with the desirable
   well-formedness check in the background, but without modification of
   the printed text.
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.
 
diff -r 79e1e99e0a2a -r 6ac8c55c657e doc-src/IsarRef/Thy/Generic.thy
--- a/doc-src/IsarRef/Thy/Generic.thy	Mon May 02 20:14:19 2011 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy	Mon May 02 20:34:34 2011 +0200
@@ -795,7 +795,7 @@
   premises of a sub-goal, using the meta-level equations declared via
   @{attribute atomize} (as an attribute) beforehand.  As a result,
   heavily nested goals become amenable to fundamental operations such
-  as resolution (cf.\ the @{method rule} method).  Giving the ``@{text
+  as resolution (cf.\ the @{method (Pure) rule} method).  Giving the ``@{text
   "(full)"}'' option here means to turn the whole subgoal into an
   object-statement (if possible), including the outermost parameters
   and assumptions as well.
diff -r 79e1e99e0a2a -r 6ac8c55c657e doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon May 02 20:14:19 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon May 02 20:34:34 2011 +0200
@@ -896,7 +896,7 @@
   ``@{text "!"}'' indicator refers to ``safe'' rules, which may be
   applied aggressively (without considering back-tracking later).
   Rules declared with ``@{text "?"}'' are ignored in proof search (the
-  single-step @{method rule} method still observes these).  An
+  single-step @{method (Pure) rule} method still observes these).  An
   explicit weight annotation may be given as well; otherwise the
   number of rule premises will be taken into account here.
 *}
@@ -1419,7 +1419,7 @@
     @{command_def (HOL) "code_library"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def (HOL) "consts_code"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def (HOL) "types_code"} & : & @{text "theory \<rightarrow> theory"} \\
-    @{attribute_def (HOL) code} & : & @{text attribute} \\
+    @{attribute_def code} & : & @{text attribute} \\
   \end{matharray}
 
   @{rail "
@@ -1452,7 +1452,7 @@
   attachment: 'attach' modespec? '{' @{syntax text} '}'
   ;
 
-  @@{attribute (HOL) code} (name)?
+  @@{attribute code} name?
   "}
 *}
 
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.
diff -r 79e1e99e0a2a -r 6ac8c55c657e doc-src/IsarRef/Thy/Proof.thy
--- a/doc-src/IsarRef/Thy/Proof.thy	Mon May 02 20:14:19 2011 +0200
+++ b/doc-src/IsarRef/Thy/Proof.thy	Mon May 02 20:34:34 2011 +0200
@@ -339,7 +339,7 @@
   facts in order to establish the goal to be claimed next.  The
   initial proof method invoked to refine that will be offered the
   facts to do ``anything appropriate'' (see also
-  \secref{sec:proof-steps}).  For example, method @{method_ref rule}
+  \secref{sec:proof-steps}).  For example, method @{method (Pure) rule}
   (see \secref{sec:pure-meth-att}) would typically do an elimination
   rather than an introduction.  Automatic methods usually insert the
   facts into the goal state before operation.  This provides a simple
@@ -368,7 +368,7 @@
   effect apart from entering @{text "prove(chain)"} mode, since
   @{fact_ref nothing} is bound to the empty list of theorems.
 
-  Basic proof methods (such as @{method_ref rule}) expect multiple
+  Basic proof methods (such as @{method_ref (Pure) rule}) expect multiple
   facts to be given in their proper order, corresponding to a prefix
   of the premises of the rule involved.  Note that positions may be
   easily skipped using something like @{command "from"}~@{text "_
@@ -618,10 +618,11 @@
   an intelligible manner.
 
   Unless given explicitly by the user, the default initial method is
-  ``@{method_ref rule}'', which applies a single standard elimination
-  or introduction rule according to the topmost symbol involved.
-  There is no separate default terminal method.  Any remaining goals
-  are always solved by assumption in the very last step.
+  @{method_ref (Pure) rule} (or its classical variant @{method_ref
+  rule}), which applies a single standard elimination or introduction
+  rule according to the topmost symbol involved.  There is no separate
+  default terminal method.  Any remaining goals are always solved by
+  assumption in the very last step.
 
   @{rail "
     @@{command proof} method?
@@ -697,11 +698,11 @@
     @{method_def "fact"} & : & @{text method} \\
     @{method_def "assumption"} & : & @{text method} \\
     @{method_def "this"} & : & @{text method} \\
-    @{method_def "rule"} & : & @{text method} \\
+    @{method_def (Pure) "rule"} & : & @{text method} \\
     @{attribute_def (Pure) "intro"} & : & @{text attribute} \\
     @{attribute_def (Pure) "elim"} & : & @{text attribute} \\
     @{attribute_def (Pure) "dest"} & : & @{text attribute} \\
-    @{attribute_def "rule"} & : & @{text attribute} \\[0.5ex]
+    @{attribute_def (Pure) "rule"} & : & @{text attribute} \\[0.5ex]
     @{attribute_def "OF"} & : & @{text attribute} \\
     @{attribute_def "of"} & : & @{text attribute} \\
     @{attribute_def "where"} & : & @{text attribute} \\
@@ -710,7 +711,7 @@
   @{rail "
     @@{method fact} @{syntax thmrefs}?
     ;
-    @@{method rule} @{syntax thmrefs}?
+    @@{method (Pure) rule} @{syntax thmrefs}?
     ;
     rulemod: ('intro' | 'elim' | 'dest')
       ((('!' | () | '?') @{syntax nat}?) | 'del') ':' @{syntax thmrefs}
@@ -718,7 +719,7 @@
     (@@{attribute intro} | @@{attribute elim} | @@{attribute dest})
       ('!' | () | '?') @{syntax nat}?
     ;
-    @@{attribute rule} 'del'
+    @@{attribute (Pure) rule} 'del'
     ;
     @@{attribute OF} @{syntax thmrefs}
     ;
@@ -734,7 +735,7 @@
   \item ``@{method "-"}'' (minus) does nothing but insert the forward
   chaining facts as premises into the goal.  Note that command
   @{command_ref "proof"} without any method actually performs a single
-  reduction step using the @{method_ref rule} method; thus a plain
+  reduction step using the @{method_ref (Pure) rule} method; thus a plain
   \emph{do-nothing} proof step would be ``@{command "proof"}~@{text
   "-"}'' rather than @{command "proof"} alone.
   
@@ -761,12 +762,12 @@
   rules.  Recall that ``@{command "."}'' (dot) abbreviates ``@{command
   "by"}~@{text this}''.
   
-  \item @{method rule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} applies some rule given as
+  \item @{method (Pure) rule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} applies some rule given as
   argument in backward manner; facts are used to reduce the rule
-  before applying it to the goal.  Thus @{method rule} without facts
+  before applying it to the goal.  Thus @{method (Pure) rule} without facts
   is plain introduction, while with facts it becomes elimination.
   
-  When no arguments are given, the @{method rule} method tries to pick
+  When no arguments are given, the @{method (Pure) rule} method tries to pick
   appropriate rules automatically, as declared in the current context
   using the @{attribute (Pure) intro}, @{attribute (Pure) elim},
   @{attribute (Pure) dest} attributes (see below).  This is the
@@ -775,7 +776,7 @@
   
   \item @{attribute (Pure) intro}, @{attribute (Pure) elim}, and
   @{attribute (Pure) dest} declare introduction, elimination, and
-  destruct rules, to be used with method @{method rule}, and similar
+  destruct rules, to be used with method @{method (Pure) rule}, and similar
   tools.  Note that the latter will ignore rules declared with
   ``@{text "?"}'', while ``@{text "!"}''  are used most aggressively.
   
@@ -784,7 +785,7 @@
   present versions of Isabelle/Pure, i.e.\ @{attribute (Pure)
   "Pure.intro"}.
   
-  \item @{attribute rule}~@{text del} undeclares introduction,
+  \item @{attribute (Pure) rule}~@{text del} undeclares introduction,
   elimination, or destruct rules.
   
   \item @{attribute OF}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} applies some
diff -r 79e1e99e0a2a -r 6ac8c55c657e doc-src/IsarRef/Thy/Spec.thy
--- a/doc-src/IsarRef/Thy/Spec.thy	Mon May 02 20:14:19 2011 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy	Mon May 02 20:34:34 2011 +0200
@@ -631,7 +631,7 @@
     @{command_def "class"} & : & @{text "theory \<rightarrow> local_theory"} \\
     @{command_def "instantiation"} & : & @{text "theory \<rightarrow> local_theory"} \\
     @{command_def "instance"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
-    @{command_def "instance"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
+    @{command "instance"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
     @{command_def "subclass"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "print_classes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{command_def "class_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
diff -r 79e1e99e0a2a -r 6ac8c55c657e doc-src/IsarRef/Thy/document/Document_Preparation.tex
--- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Mon May 02 20:14:19 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Mon May 02 20:34:34 2011 +0200
@@ -553,7 +553,7 @@
   not under direct control of the author, it may even fluctuate a bit
   as the underlying theory is changed later on.
 
-  In contrast, \indexdef{}{antiquotation option}{source}\hypertarget{antiquotation option.source}{\hyperlink{antiquotation option.source}{\mbox{\isa{source}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ true{\isaliteral{22}{\isachardoublequote}}}
+  In contrast, \hyperlink{antiquotation option.source}{\mbox{\isa{source}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ true{\isaliteral{22}{\isachardoublequote}}}
   admits direct printing of the given source text, with the desirable
   well-formedness check in the background, but without modification of
   the printed text.
diff -r 79e1e99e0a2a -r 6ac8c55c657e doc-src/IsarRef/Thy/document/Framework.tex
--- a/doc-src/IsarRef/Thy/document/Framework.tex	Mon May 02 20:14:19 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Framework.tex	Mon May 02 20:34:34 2011 +0200
@@ -632,19 +632,19 @@
   populated later.  Methods use the facts indicated by \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}} or \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}}, and then operate on the goal state.
   Some basic methods are predefined: ``\hyperlink{method.-}{\mbox{\isa{{\isaliteral{2D}{\isacharminus}}}}}'' leaves the goal
   unchanged, ``\hyperlink{method.this}{\mbox{\isa{this}}}'' applies the facts as rules to the
-  goal, ``\hyperlink{method.rule}{\mbox{\isa{rule}}}'' applies the facts to another rule and the
-  result to the goal (both ``\hyperlink{method.this}{\mbox{\isa{this}}}'' and ``\hyperlink{method.rule}{\mbox{\isa{rule}}}''
+  goal, ``\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}'' applies the facts to another rule and the
+  result to the goal (both ``\hyperlink{method.this}{\mbox{\isa{this}}}'' and ``\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}''
   refer to \hyperlink{inference.resolution}{\mbox{\isa{resolution}}} of
   \secref{sec:framework-resolution}).  The secondary arguments to
-  ``\hyperlink{method.rule}{\mbox{\isa{rule}}}'' may be specified explicitly as in ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}rule\ a{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'', or picked from the context.  In the latter case, the system
+  ``\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}'' may be specified explicitly as in ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}rule\ a{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'', or picked from the context.  In the latter case, the system
   first tries rules declared as \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}} or
   \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}, followed by those declared as \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}.
 
-  The default method for \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}} is ``\hyperlink{method.rule}{\mbox{\isa{rule}}}''
+  The default method for \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}} is ``\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}''
   (arguments picked from the context), for \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}} it is
   ``\hyperlink{method.-}{\mbox{\isa{{\isaliteral{2D}{\isacharminus}}}}}''.  Further abbreviations for terminal proof steps
   are ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}method\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ method\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}}'' for
-  ``\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}method\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}method\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}}'', and ``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}}}}'' for ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\hyperlink{method.rule}{\mbox{\isa{rule}}}, and ``\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}}}}}'' for ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\hyperlink{method.this}{\mbox{\isa{this}}}''.  The \hyperlink{command.unfolding}{\mbox{\isa{\isacommand{unfolding}}}} element operates
+  ``\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}method\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}method\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}}'', and ``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}}}}'' for ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}, and ``\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}}}}}'' for ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\hyperlink{method.this}{\mbox{\isa{this}}}''.  The \hyperlink{command.unfolding}{\mbox{\isa{\isacommand{unfolding}}}} element operates
   directly on the current facts and goal by applying equalities.
 
   \medskip Block structure can be indicated explicitly by ``\hyperlink{command.braceleft}{\mbox{\isa{\isacommand{{\isaliteral{7B}{\isacharbraceleft}}}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}~\hyperlink{command.braceright}{\mbox{\isa{\isacommand{{\isaliteral{7D}{\isacharbraceright}}}}}}'', although the body of a sub-proof
diff -r 79e1e99e0a2a -r 6ac8c55c657e doc-src/IsarRef/Thy/document/Generic.tex
--- a/doc-src/IsarRef/Thy/document/Generic.tex	Mon May 02 20:14:19 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex	Mon May 02 20:34:34 2011 +0200
@@ -1286,7 +1286,7 @@
   premises of a sub-goal, using the meta-level equations declared via
   \hyperlink{attribute.atomize}{\mbox{\isa{atomize}}} (as an attribute) beforehand.  As a result,
   heavily nested goals become amenable to fundamental operations such
-  as resolution (cf.\ the \hyperlink{method.rule}{\mbox{\isa{rule}}} method).  Giving the ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}full{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' option here means to turn the whole subgoal into an
+  as resolution (cf.\ the \hyperlink{method.Pure.rule}{\mbox{\isa{rule}}} method).  Giving the ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}full{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' option here means to turn the whole subgoal into an
   object-statement (if possible), including the outermost parameters
   and assumptions as well.
 
diff -r 79e1e99e0a2a -r 6ac8c55c657e doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon May 02 20:14:19 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon May 02 20:34:34 2011 +0200
@@ -1230,7 +1230,7 @@
   ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{21}{\isacharbang}}{\isaliteral{22}{\isachardoublequote}}}'' indicator refers to ``safe'' rules, which may be
   applied aggressively (without considering back-tracking later).
   Rules declared with ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}'' are ignored in proof search (the
-  single-step \hyperlink{method.rule}{\mbox{\isa{rule}}} method still observes these).  An
+  single-step \hyperlink{method.Pure.rule}{\mbox{\isa{rule}}} method still observes these).  An
   explicit weight annotation may be given as well; otherwise the
   number of rule premises will be taken into account here.%
 \end{isamarkuptext}%
@@ -2167,7 +2167,7 @@
     \indexdef{HOL}{command}{code\_library}\hypertarget{command.HOL.code-library}{\hyperlink{command.HOL.code-library}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}library}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
     \indexdef{HOL}{command}{consts\_code}\hypertarget{command.HOL.consts-code}{\hyperlink{command.HOL.consts-code}{\mbox{\isa{\isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
     \indexdef{HOL}{command}{types\_code}\hypertarget{command.HOL.types-code}{\hyperlink{command.HOL.types-code}{\mbox{\isa{\isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
-    \indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isa{attribute} \\
+    \indexdef{}{attribute}{code}\hypertarget{attribute.code}{\hyperlink{attribute.code}{\mbox{\isa{code}}}} & : & \isa{attribute} \\
   \end{matharray}
 
   \begin{railoutput}
@@ -2272,7 +2272,7 @@
 \rail@term{\isa{{\isaliteral{7D}{\isacharbraceright}}}}[]
 \rail@end
 \rail@begin{2}{\isa{}}
-\rail@term{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}}[]
+\rail@term{\hyperlink{attribute.code}{\mbox{\isa{code}}}}[]
 \rail@bar
 \rail@nextbar{1}
 \rail@nont{\isa{name}}[]
diff -r 79e1e99e0a2a -r 6ac8c55c657e doc-src/IsarRef/Thy/document/ML_Tactic.tex
--- 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.
diff -r 79e1e99e0a2a -r 6ac8c55c657e doc-src/IsarRef/Thy/document/Proof.tex
--- a/doc-src/IsarRef/Thy/document/Proof.tex	Mon May 02 20:14:19 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Proof.tex	Mon May 02 20:34:34 2011 +0200
@@ -445,7 +445,7 @@
   facts in order to establish the goal to be claimed next.  The
   initial proof method invoked to refine that will be offered the
   facts to do ``anything appropriate'' (see also
-  \secref{sec:proof-steps}).  For example, method \indexref{}{method}{rule}\hyperlink{method.rule}{\mbox{\isa{rule}}}
+  \secref{sec:proof-steps}).  For example, method \hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}
   (see \secref{sec:pure-meth-att}) would typically do an elimination
   rather than an introduction.  Automatic methods usually insert the
   facts into the goal state before operation.  This provides a simple
@@ -472,7 +472,7 @@
   effect apart from entering \isa{{\isaliteral{22}{\isachardoublequote}}prove{\isaliteral{28}{\isacharparenleft}}chain{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} mode, since
   \indexref{}{fact}{nothing}\hyperlink{fact.nothing}{\mbox{\isa{nothing}}} is bound to the empty list of theorems.
 
-  Basic proof methods (such as \indexref{}{method}{rule}\hyperlink{method.rule}{\mbox{\isa{rule}}}) expect multiple
+  Basic proof methods (such as \indexref{Pure}{method}{rule}\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}) expect multiple
   facts to be given in their proper order, corresponding to a prefix
   of the premises of the rule involved.  Note that positions may be
   easily skipped using something like \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{5C3C414E443E}{\isasymAND}}\ a\ {\isaliteral{5C3C414E443E}{\isasymAND}}\ b{\isaliteral{22}{\isachardoublequote}}}, for example.  This involves the trivial rule
@@ -843,10 +843,10 @@
   an intelligible manner.
 
   Unless given explicitly by the user, the default initial method is
-  ``\indexref{}{method}{rule}\hyperlink{method.rule}{\mbox{\isa{rule}}}'', which applies a single standard elimination
-  or introduction rule according to the topmost symbol involved.
-  There is no separate default terminal method.  Any remaining goals
-  are always solved by assumption in the very last step.
+  \indexref{Pure}{method}{rule}\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}} (or its classical variant \indexref{}{method}{rule}\hyperlink{method.rule}{\mbox{\isa{rule}}}), which applies a single standard elimination or introduction
+  rule according to the topmost symbol involved.  There is no separate
+  default terminal method.  Any remaining goals are always solved by
+  assumption in the very last step.
 
   \begin{railoutput}
 \rail@begin{2}{\isa{}}
@@ -943,11 +943,11 @@
     \indexdef{}{method}{fact}\hypertarget{method.fact}{\hyperlink{method.fact}{\mbox{\isa{fact}}}} & : & \isa{method} \\
     \indexdef{}{method}{assumption}\hypertarget{method.assumption}{\hyperlink{method.assumption}{\mbox{\isa{assumption}}}} & : & \isa{method} \\
     \indexdef{}{method}{this}\hypertarget{method.this}{\hyperlink{method.this}{\mbox{\isa{this}}}} & : & \isa{method} \\
-    \indexdef{}{method}{rule}\hypertarget{method.rule}{\hyperlink{method.rule}{\mbox{\isa{rule}}}} & : & \isa{method} \\
+    \indexdef{Pure}{method}{rule}\hypertarget{method.Pure.rule}{\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}} & : & \isa{method} \\
     \indexdef{Pure}{attribute}{intro}\hypertarget{attribute.Pure.intro}{\hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}} & : & \isa{attribute} \\
     \indexdef{Pure}{attribute}{elim}\hypertarget{attribute.Pure.elim}{\hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}} & : & \isa{attribute} \\
     \indexdef{Pure}{attribute}{dest}\hypertarget{attribute.Pure.dest}{\hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}} & : & \isa{attribute} \\
-    \indexdef{}{attribute}{rule}\hypertarget{attribute.rule}{\hyperlink{attribute.rule}{\mbox{\isa{rule}}}} & : & \isa{attribute} \\[0.5ex]
+    \indexdef{Pure}{attribute}{rule}\hypertarget{attribute.Pure.rule}{\hyperlink{attribute.Pure.rule}{\mbox{\isa{rule}}}} & : & \isa{attribute} \\[0.5ex]
     \indexdef{}{attribute}{OF}\hypertarget{attribute.OF}{\hyperlink{attribute.OF}{\mbox{\isa{OF}}}} & : & \isa{attribute} \\
     \indexdef{}{attribute}{of}\hypertarget{attribute.of}{\hyperlink{attribute.of}{\mbox{\isa{of}}}} & : & \isa{attribute} \\
     \indexdef{}{attribute}{where}\hypertarget{attribute.where}{\hyperlink{attribute.where}{\mbox{\isa{where}}}} & : & \isa{attribute} \\
@@ -962,7 +962,7 @@
 \rail@endbar
 \rail@end
 \rail@begin{2}{\isa{}}
-\rail@term{\hyperlink{method.rule}{\mbox{\isa{rule}}}}[]
+\rail@term{\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}}[]
 \rail@bar
 \rail@nextbar{1}
 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
@@ -1013,7 +1013,7 @@
 \rail@endbar
 \rail@end
 \rail@begin{1}{\isa{}}
-\rail@term{\hyperlink{attribute.rule}{\mbox{\isa{rule}}}}[]
+\rail@term{\hyperlink{attribute.Pure.rule}{\mbox{\isa{rule}}}}[]
 \rail@term{\isa{del}}[]
 \rail@end
 \rail@begin{1}{\isa{}}
@@ -1063,7 +1063,7 @@
   \item ``\hyperlink{method.-}{\mbox{\isa{{\isaliteral{2D}{\isacharminus}}}}}'' (minus) does nothing but insert the forward
   chaining facts as premises into the goal.  Note that command
   \indexref{}{command}{proof}\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}} without any method actually performs a single
-  reduction step using the \indexref{}{method}{rule}\hyperlink{method.rule}{\mbox{\isa{rule}}} method; thus a plain
+  reduction step using the \indexref{Pure}{method}{rule}\hyperlink{method.Pure.rule}{\mbox{\isa{rule}}} method; thus a plain
   \emph{do-nothing} proof step would be ``\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{22}{\isachardoublequote}}}'' rather than \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}} alone.
   
   \item \hyperlink{method.fact}{\mbox{\isa{fact}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} composes some fact from
@@ -1086,12 +1086,12 @@
   \item \hyperlink{method.this}{\mbox{\isa{this}}} applies all of the current facts directly as
   rules.  Recall that ``\hyperlink{command.dot}{\mbox{\isa{\isacommand{{\isaliteral{2E}{\isachardot}}}}}}'' (dot) abbreviates ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{this}''.
   
-  \item \hyperlink{method.rule}{\mbox{\isa{rule}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} applies some rule given as
+  \item \hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} applies some rule given as
   argument in backward manner; facts are used to reduce the rule
-  before applying it to the goal.  Thus \hyperlink{method.rule}{\mbox{\isa{rule}}} without facts
+  before applying it to the goal.  Thus \hyperlink{method.Pure.rule}{\mbox{\isa{rule}}} without facts
   is plain introduction, while with facts it becomes elimination.
   
-  When no arguments are given, the \hyperlink{method.rule}{\mbox{\isa{rule}}} method tries to pick
+  When no arguments are given, the \hyperlink{method.Pure.rule}{\mbox{\isa{rule}}} method tries to pick
   appropriate rules automatically, as declared in the current context
   using the \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}, \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}},
   \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}} attributes (see below).  This is the
@@ -1100,7 +1100,7 @@
   
   \item \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}, \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, and
   \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}} declare introduction, elimination, and
-  destruct rules, to be used with method \hyperlink{method.rule}{\mbox{\isa{rule}}}, and similar
+  destruct rules, to be used with method \hyperlink{method.Pure.rule}{\mbox{\isa{rule}}}, and similar
   tools.  Note that the latter will ignore rules declared with
   ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}'', while ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{21}{\isacharbang}}{\isaliteral{22}{\isachardoublequote}}}''  are used most aggressively.
   
@@ -1108,7 +1108,7 @@
   own variants of these attributes; use qualified names to access the
   present versions of Isabelle/Pure, i.e.\ \hyperlink{attribute.Pure.Pure.intro}{\mbox{\isa{Pure{\isaliteral{2E}{\isachardot}}intro}}}.
   
-  \item \hyperlink{attribute.rule}{\mbox{\isa{rule}}}~\isa{del} undeclares introduction,
+  \item \hyperlink{attribute.Pure.rule}{\mbox{\isa{rule}}}~\isa{del} undeclares introduction,
   elimination, or destruct rules.
   
   \item \hyperlink{attribute.OF}{\mbox{\isa{OF}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} applies some
diff -r 79e1e99e0a2a -r 6ac8c55c657e doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Mon May 02 20:14:19 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Mon May 02 20:34:34 2011 +0200
@@ -957,7 +957,7 @@
     \indexdef{}{command}{class}\hypertarget{command.class}{\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
     \indexdef{}{command}{instantiation}\hypertarget{command.instantiation}{\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
     \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
-    \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
+    \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
     \indexdef{}{command}{subclass}\hypertarget{command.subclass}{\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
     \indexdef{}{command}{print\_classes}\hypertarget{command.print-classes}{\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}classes}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
     \indexdef{}{command}{class\_deps}\hypertarget{command.class-deps}{\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isaliteral{5F}{\isacharunderscore}}deps}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\