1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon May 02 20:14:19 2011 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon May 02 20:34:34 2011 +0200
     1.3 @@ -896,7 +896,7 @@
     1.4    ``@{text "!"}'' indicator refers to ``safe'' rules, which may be
     1.5    applied aggressively (without considering back-tracking later).
     1.6    Rules declared with ``@{text "?"}'' are ignored in proof search (the
     1.7 -  single-step @{method rule} method still observes these).  An
     1.8 +  single-step @{method (Pure) rule} method still observes these).  An
     1.9    explicit weight annotation may be given as well; otherwise the
    1.10    number of rule premises will be taken into account here.
    1.11  *}
    1.12 @@ -1419,7 +1419,7 @@
    1.13      @{command_def (HOL) "code_library"} & : & @{text "theory \<rightarrow> theory"} \\
    1.14      @{command_def (HOL) "consts_code"} & : & @{text "theory \<rightarrow> theory"} \\
    1.15      @{command_def (HOL) "types_code"} & : & @{text "theory \<rightarrow> theory"} \\
    1.16 -    @{attribute_def (HOL) code} & : & @{text attribute} \\
    1.17 +    @{attribute_def code} & : & @{text attribute} \\
    1.18    \end{matharray}
    1.19  
    1.20    @{rail "
    1.21 @@ -1452,7 +1452,7 @@
    1.22    attachment: 'attach' modespec? '{' @{syntax text} '}'
    1.23    ;
    1.24  
    1.25 -  @@{attribute (HOL) code} (name)?
    1.26 +  @@{attribute code} name?
    1.27    "}
    1.28  *}
    1.29