1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed May 14 20:31:17 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed May 14 20:31:41 2008 +0200
     1.3 @@ -69,9 +69,10 @@
     1.4    corresponding injection/surjection pair (in both directions).  Rules
     1.5    \isa{Rep{\isacharunderscore}t{\isacharunderscore}inject} and \isa{Abs{\isacharunderscore}t{\isacharunderscore}inject} provide a slightly
     1.6    more convenient view on the injectivity part, suitable for automated
     1.7 -  proof tools (e.g.\ in \mbox{\isa{simp}} or \mbox{\isa{iff}} declarations).
     1.8 -  Rules \isa{Rep{\isacharunderscore}t{\isacharunderscore}cases}/\isa{Rep{\isacharunderscore}t{\isacharunderscore}induct}, and \isa{Abs{\isacharunderscore}t{\isacharunderscore}cases}/\isa{Abs{\isacharunderscore}t{\isacharunderscore}induct} provide alternative views on
     1.9 -  surjectivity; these are already declared as set or type rules for
    1.10 +  proof tools (e.g.\ in \mbox{\isa{simp}} or \mbox{\isa{iff}}
    1.11 +  declarations).  Rules \isa{Rep{\isacharunderscore}t{\isacharunderscore}cases}/\isa{Rep{\isacharunderscore}t{\isacharunderscore}induct}, and
    1.12 +  \isa{Abs{\isacharunderscore}t{\isacharunderscore}cases}/\isa{Abs{\isacharunderscore}t{\isacharunderscore}induct} provide alternative views
    1.13 +  on surjectivity; these are already declared as set or type rules for
    1.14    the generic \mbox{\isa{cases}} and \mbox{\isa{induct}} methods.
    1.15    
    1.16    An alternative name may be specified in parentheses; the default is
    1.17 @@ -817,15 +818,15 @@
    1.18  \begin{isamarkuptext}%
    1.19  \begin{matharray}{rcl}
    1.20      \indexdef{HOL}{method}{arith}\mbox{\isa{arith}} & : & \isarmeth \\
    1.21 -    \indexdef{HOL}{method}{arith\_split}\mbox{\isa{arith{\isacharunderscore}split}} & : & \isaratt \\
    1.22 +    \indexdef{HOL}{attribute}{arith\_split}\mbox{\isa{arith{\isacharunderscore}split}} & : & \isaratt \\
    1.23    \end{matharray}
    1.24  
    1.25    The \mbox{\isa{arith}} method decides linear arithmetic problems
    1.26    (on types \isa{nat}, \isa{int}, \isa{real}).  Any current
    1.27    facts are inserted into the goal before running the procedure.
    1.28  
    1.29 -  The \mbox{\isa{arith{\isacharunderscore}split}} attribute declares case split rules
    1.30 -  to be expanded before the arithmetic procedure is invoked.
    1.31 +  The \mbox{\isa{arith{\isacharunderscore}split}} attribute declares case split
    1.32 +  rules to be expanded before the arithmetic procedure is invoked.
    1.33  
    1.34    Note that a simpler (but faster) version of arithmetic reasoning is
    1.35    already performed by the Simplifier.%