1.1 --- a/doc-src/IsarRef/Thy/Generic.thy	Thu May 15 17:37:20 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Generic.thy	Thu May 15 17:37:21 2008 +0200
     1.3 @@ -1325,11 +1325,11 @@
     1.4    facts, which are guaranteed to participate, may appear in either
     1.5    order.
     1.6  
     1.7 -  \item [@{attribute intro} and @{attribute elim}] repeatedly refine
     1.8 -  some goal by intro- or elim-resolution, after having inserted any
     1.9 -  chained facts.  Exactly the rules given as arguments are taken into
    1.10 -  account; this allows fine-tuned decomposition of a proof problem, in
    1.11 -  contrast to common automated tools.
    1.12 +  \item [@{method intro} and @{method elim}] repeatedly refine some
    1.13 +  goal by intro- or elim-resolution, after having inserted any chained
    1.14 +  facts.  Exactly the rules given as arguments are taken into account;
    1.15 +  this allows fine-tuned decomposition of a proof problem, in contrast
    1.16 +  to common automated tools.
    1.17  
    1.18    \end{descr}
    1.19  *}

     2.1 --- a/doc-src/IsarRef/Thy/Proof.thy	Thu May 15 17:37:20 2008 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/Proof.thy	Thu May 15 17:37:21 2008 +0200
     2.3 @@ -495,9 +495,9 @@
     2.4      @{method_def "this"} & : & \isarmeth \\
     2.5      @{method_def "rule"} & : & \isarmeth \\
     2.6      @{method_def "iprover"} & : & \isarmeth \\[0.5ex]
     2.7 -    @{attribute_def "intro"} & : & \isaratt \\
     2.8 -    @{attribute_def "elim"} & : & \isaratt \\
     2.9 -    @{attribute_def "dest"} & : & \isaratt \\
    2.10 +    @{attribute_def (Pure) "intro"} & : & \isaratt \\
    2.11 +    @{attribute_def (Pure) "elim"} & : & \isaratt \\
    2.12 +    @{attribute_def (Pure) "dest"} & : & \isaratt \\
    2.13      @{attribute_def "rule"} & : & \isaratt \\[0.5ex]
    2.14      @{attribute_def "OF"} & : & \isaratt \\
    2.15      @{attribute_def "of"} & : & \isaratt \\
    2.16 @@ -565,10 +565,10 @@
    2.17    
    2.18    When no arguments are given, the @{method rule} method tries to pick
    2.19    appropriate rules automatically, as declared in the current context
    2.20 -  using the @{attribute intro}, @{attribute elim}, @{attribute dest}
    2.21 -  attributes (see below).  This is the default behavior of @{command
    2.22 -  "proof"} and ``@{command ".."}'' (double-dot) steps (see
    2.23 -  \secref{sec:proof-steps}).
    2.24 +  using the @{attribute (Pure) intro}, @{attribute (Pure) elim},
    2.25 +  @{attribute (Pure) dest} attributes (see below).  This is the
    2.26 +  default behavior of @{command "proof"} and ``@{command ".."}'' 
    2.27 +  (double-dot) steps (see \secref{sec:proof-steps}).
    2.28    
    2.29    \item [@{method iprover}] performs intuitionistic proof search,
    2.30    depending on specifically declared rules from the context, or given
    2.31 @@ -576,24 +576,26 @@
    2.32    before commencing proof search; ``@{method iprover}@{text "!"}'' 
    2.33    means to include the current @{fact prems} as well.
    2.34    
    2.35 -  Rules need to be classified as @{attribute intro}, @{attribute
    2.36 -  elim}, or @{attribute dest}; here the ``@{text "!"}'' indicator
    2.37 -  refers to ``safe'' rules, which may be applied aggressively (without
    2.38 -  considering back-tracking later).  Rules declared with ``@{text
    2.39 -  "?"}'' are ignored in proof search (the single-step @{method rule}
    2.40 -  method still observes these).  An explicit weight annotation may be
    2.41 -  given as well; otherwise the number of rule premises will be taken
    2.42 -  into account here.
    2.43 +  Rules need to be classified as @{attribute (Pure) intro},
    2.44 +  @{attribute (Pure) elim}, or @{attribute (Pure) dest}; here the
    2.45 +  ``@{text "!"}'' indicator refers to ``safe'' rules, which may be
    2.46 +  applied aggressively (without considering back-tracking later).
    2.47 +  Rules declared with ``@{text "?"}'' are ignored in proof search (the
    2.48 +  single-step @{method rule} method still observes these).  An
    2.49 +  explicit weight annotation may be given as well; otherwise the
    2.50 +  number of rule premises will be taken into account here.
    2.51    
    2.52 -  \item [@{attribute intro}, @{attribute elim}, and @{attribute dest}]
    2.53 -  declare introduction, elimination, and destruct rules, to be used
    2.54 -  with the @{method rule} and @{method iprover} methods.  Note that
    2.55 -  the latter will ignore rules declared with ``@{text "?"}'', while
    2.56 -  ``@{text "!"}''  are used most aggressively.
    2.57 +  \item [@{attribute (Pure) intro}, @{attribute (Pure) elim}, and
    2.58 +  @{attribute (Pure) dest}] declare introduction, elimination, and
    2.59 +  destruct rules, to be used with the @{method rule} and @{method
    2.60 +  iprover} methods.  Note that the latter will ignore rules declared
    2.61 +  with ``@{text "?"}'', while ``@{text "!"}''  are used most
    2.62 +  aggressively.
    2.63    
    2.64    The classical reasoner (see \secref{sec:classical}) introduces its
    2.65    own variants of these attributes; use qualified names to access the
    2.66 -  present versions of Isabelle/Pure, i.e.\ @{attribute "Pure.intro"}.
    2.67 +  present versions of Isabelle/Pure, i.e.\ @{attribute (Pure)
    2.68 +  "Pure.intro"}.
    2.69    
    2.70    \item [@{attribute rule}~@{text del}] undeclares introduction,
    2.71    elimination, or destruct rules.