1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed May 14 20:30:53 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed May 14 20:31:17 2008 +0200
     1.3 @@ -53,10 +53,10 @@
     1.4    corresponding injection/surjection pair (in both directions).  Rules
     1.5    @{text Rep_t_inject} and @{text Abs_t_inject} provide a slightly
     1.6    more convenient view on the injectivity part, suitable for automated
     1.7 -  proof tools (e.g.\ in @{method simp} or @{method iff} declarations).
     1.8 -  Rules @{text Rep_t_cases}/@{text Rep_t_induct}, and @{text
     1.9 -  Abs_t_cases}/@{text Abs_t_induct} provide alternative views on
    1.10 -  surjectivity; these are already declared as set or type rules for
    1.11 +  proof tools (e.g.\ in @{attribute simp} or @{attribute iff}
    1.12 +  declarations).  Rules @{text Rep_t_cases}/@{text Rep_t_induct}, and
    1.13 +  @{text Abs_t_cases}/@{text Abs_t_induct} provide alternative views
    1.14 +  on surjectivity; these are already declared as set or type rules for
    1.15    the generic @{method cases} and @{method induct} methods.
    1.16    
    1.17    An alternative name may be specified in parentheses; the default is
    1.18 @@ -89,7 +89,7 @@
    1.19  
    1.20    \begin{descr}
    1.21    
    1.22 -  \item [@{method (HOL) split_format}~@{text "p\<^sub>1 \<dots> p\<^sub>m
    1.23 +  \item [@{attribute (HOL) split_format}~@{text "p\<^sub>1 \<dots> p\<^sub>m
    1.24    \<AND> \<dots> \<AND> q\<^sub>1 \<dots> q\<^sub>n"}] puts expressions of
    1.25    low-level tuple types into canonical form as specified by the
    1.26    arguments given; the @{text i}-th collection of arguments refers to
    1.27 @@ -813,15 +813,15 @@
    1.28  text {*
    1.29    \begin{matharray}{rcl}
    1.30      @{method_def (HOL) arith} & : & \isarmeth \\
    1.31 -    @{method_def (HOL) arith_split} & : & \isaratt \\
    1.32 +    @{attribute_def (HOL) arith_split} & : & \isaratt \\
    1.33    \end{matharray}
    1.34  
    1.35    The @{method (HOL) arith} method decides linear arithmetic problems
    1.36    (on types @{text nat}, @{text int}, @{text real}).  Any current
    1.37    facts are inserted into the goal before running the procedure.
    1.38  
    1.39 -  The @{method (HOL) arith_split} attribute declares case split rules
    1.40 -  to be expanded before the arithmetic procedure is invoked.
    1.41 +  The @{attribute (HOL) arith_split} attribute declares case split
    1.42 +  rules to be expanded before the arithmetic procedure is invoked.
    1.43  
    1.44    Note that a simpler (but faster) version of arithmetic reasoning is
    1.45    already performed by the Simplifier.