diff -r 1120f6cc10b0 -r d066f9db833b doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed May 14 20:31:17 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed May 14 20:31:41 2008 +0200
@@ -69,9 +69,10 @@
   corresponding injection/surjection pair (in both directions).  Rules
   \isa{Rep{\isacharunderscore}t{\isacharunderscore}inject} and \isa{Abs{\isacharunderscore}t{\isacharunderscore}inject} provide a slightly
   more convenient view on the injectivity part, suitable for automated
-  proof tools (e.g.\ in \mbox{\isa{simp}} or \mbox{\isa{iff}} declarations).
-  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
-  surjectivity; these are already declared as set or type rules for
+  proof tools (e.g.\ in \mbox{\isa{simp}} or \mbox{\isa{iff}}
+  declarations).  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 surjectivity; these are already declared as set or type rules for
   the generic \mbox{\isa{cases}} and \mbox{\isa{induct}} methods.
   
   An alternative name may be specified in parentheses; the default is
@@ -817,15 +818,15 @@
 \begin{isamarkuptext}%
 \begin{matharray}{rcl}
     \indexdef{HOL}{method}{arith}\mbox{\isa{arith}} & : & \isarmeth \\
-    \indexdef{HOL}{method}{arith\_split}\mbox{\isa{arith{\isacharunderscore}split}} & : & \isaratt \\
+    \indexdef{HOL}{attribute}{arith\_split}\mbox{\isa{arith{\isacharunderscore}split}} & : & \isaratt \\
   \end{matharray}
 
   The \mbox{\isa{arith}} method decides linear arithmetic problems
   (on types \isa{nat}, \isa{int}, \isa{real}).  Any current
   facts are inserted into the goal before running the procedure.
 
-  The \mbox{\isa{arith{\isacharunderscore}split}} attribute declares case split rules
-  to be expanded before the arithmetic procedure is invoked.
+  The \mbox{\isa{arith{\isacharunderscore}split}} attribute declares case split
+  rules to be expanded before the arithmetic procedure is invoked.
 
   Note that a simpler (but faster) version of arithmetic reasoning is
   already performed by the Simplifier.%