1.1 --- a/doc-src/IsarRef/Thy/Proof.thy	Thu May 15 17:37:20 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Proof.thy	Thu May 15 17:37:21 2008 +0200
     1.3 @@ -495,9 +495,9 @@
     1.4      @{method_def "this"} & : & \isarmeth \\
     1.5      @{method_def "rule"} & : & \isarmeth \\
     1.6      @{method_def "iprover"} & : & \isarmeth \\[0.5ex]
     1.7 -    @{attribute_def "intro"} & : & \isaratt \\
     1.8 -    @{attribute_def "elim"} & : & \isaratt \\
     1.9 -    @{attribute_def "dest"} & : & \isaratt \\
    1.10 +    @{attribute_def (Pure) "intro"} & : & \isaratt \\
    1.11 +    @{attribute_def (Pure) "elim"} & : & \isaratt \\
    1.12 +    @{attribute_def (Pure) "dest"} & : & \isaratt \\
    1.13      @{attribute_def "rule"} & : & \isaratt \\[0.5ex]
    1.14      @{attribute_def "OF"} & : & \isaratt \\
    1.15      @{attribute_def "of"} & : & \isaratt \\
    1.16 @@ -565,10 +565,10 @@
    1.17    
    1.18    When no arguments are given, the @{method rule} method tries to pick
    1.19    appropriate rules automatically, as declared in the current context
    1.20 -  using the @{attribute intro}, @{attribute elim}, @{attribute dest}
    1.21 -  attributes (see below).  This is the default behavior of @{command
    1.22 -  "proof"} and ``@{command ".."}'' (double-dot) steps (see
    1.23 -  \secref{sec:proof-steps}).
    1.24 +  using the @{attribute (Pure) intro}, @{attribute (Pure) elim},
    1.25 +  @{attribute (Pure) dest} attributes (see below).  This is the
    1.26 +  default behavior of @{command "proof"} and ``@{command ".."}'' 
    1.27 +  (double-dot) steps (see \secref{sec:proof-steps}).
    1.28    
    1.29    \item [@{method iprover}] performs intuitionistic proof search,
    1.30    depending on specifically declared rules from the context, or given
    1.31 @@ -576,24 +576,26 @@
    1.32    before commencing proof search; ``@{method iprover}@{text "!"}'' 
    1.33    means to include the current @{fact prems} as well.
    1.34    
    1.35 -  Rules need to be classified as @{attribute intro}, @{attribute
    1.36 -  elim}, or @{attribute dest}; here the ``@{text "!"}'' indicator
    1.37 -  refers to ``safe'' rules, which may be applied aggressively (without
    1.38 -  considering back-tracking later).  Rules declared with ``@{text
    1.39 -  "?"}'' are ignored in proof search (the single-step @{method rule}
    1.40 -  method still observes these).  An explicit weight annotation may be
    1.41 -  given as well; otherwise the number of rule premises will be taken
    1.42 -  into account here.
    1.43 +  Rules need to be classified as @{attribute (Pure) intro},
    1.44 +  @{attribute (Pure) elim}, or @{attribute (Pure) dest}; here the
    1.45 +  ``@{text "!"}'' indicator refers to ``safe'' rules, which may be
    1.46 +  applied aggressively (without considering back-tracking later).
    1.47 +  Rules declared with ``@{text "?"}'' are ignored in proof search (the
    1.48 +  single-step @{method rule} method still observes these).  An
    1.49 +  explicit weight annotation may be given as well; otherwise the
    1.50 +  number of rule premises will be taken into account here.
    1.51    
    1.52 -  \item [@{attribute intro}, @{attribute elim}, and @{attribute dest}]
    1.53 -  declare introduction, elimination, and destruct rules, to be used
    1.54 -  with the @{method rule} and @{method iprover} methods.  Note that
    1.55 -  the latter will ignore rules declared with ``@{text "?"}'', while
    1.56 -  ``@{text "!"}''  are used most aggressively.
    1.57 +  \item [@{attribute (Pure) intro}, @{attribute (Pure) elim}, and
    1.58 +  @{attribute (Pure) dest}] declare introduction, elimination, and
    1.59 +  destruct rules, to be used with the @{method rule} and @{method
    1.60 +  iprover} methods.  Note that the latter will ignore rules declared
    1.61 +  with ``@{text "?"}'', while ``@{text "!"}''  are used most
    1.62 +  aggressively.
    1.63    
    1.64    The classical reasoner (see \secref{sec:classical}) introduces its
    1.65    own variants of these attributes; use qualified names to access the
    1.66 -  present versions of Isabelle/Pure, i.e.\ @{attribute "Pure.intro"}.
    1.67 +  present versions of Isabelle/Pure, i.e.\ @{attribute (Pure)
    1.68 +  "Pure.intro"}.
    1.69    
    1.70    \item [@{attribute rule}~@{text del}] undeclares introduction,
    1.71    elimination, or destruct rules.