doc-src/IsarRef/Thy/document/HOL_Specific.tex
changeset 30863 5dc392a59bb7
parent 30172 afdf7808cfd0
child 30865 5106e13d400f
     1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Apr 03 09:27:31 2009 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Apr 03 16:17:50 2009 +0200
     1.3 @@ -764,6 +764,7 @@
     1.4  \begin{isamarkuptext}%
     1.5  \begin{matharray}{rcl}
     1.6      \indexdef{HOL}{method}{arith}\hypertarget{method.HOL.arith}{\hyperlink{method.HOL.arith}{\mbox{\isa{arith}}}} & : & \isa{method} \\
     1.7 +    \indexdef{HOL}{attribute}{arith}\hypertarget{attribute.HOL.arith}{\hyperlink{attribute.HOL.arith}{\mbox{\isa{arith}}}} & : & \isa{attribute} \\
     1.8      \indexdef{HOL}{attribute}{arith\_split}\hypertarget{attribute.HOL.arith-split}{\hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isacharunderscore}split}}}} & : & \isa{attribute} \\
     1.9    \end{matharray}
    1.10  
    1.11 @@ -771,11 +772,14 @@
    1.12    (on types \isa{nat}, \isa{int}, \isa{real}).  Any current
    1.13    facts are inserted into the goal before running the procedure.
    1.14  
    1.15 -  The \hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isacharunderscore}split}}} attribute declares case split
    1.16 -  rules to be expanded before the arithmetic procedure is invoked.
    1.17 +  The \hyperlink{attribute.HOL.arith}{\mbox{\isa{arith}}} attribute declares facts that are
    1.18 +  always supplied to the arithmetic provers implicitly.
    1.19  
    1.20 -  Note that a simpler (but faster) version of arithmetic reasoning is
    1.21 -  already performed by the Simplifier.%
    1.22 +  The \hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isacharunderscore}split}}} attribute declares case split
    1.23 +  rules to be expanded before \indexdef{HOL}{method}{arith}\hypertarget{method.HOL.arith}{\hyperlink{method.HOL.arith}{\mbox{\isa{arith}}}} is invoked.
    1.24 +
    1.25 +  Note that a simpler (but faster) arithmetic prover is
    1.26 +  already invoked by the Simplifier.%
    1.27  \end{isamarkuptext}%
    1.28  \isamarkuptrue%
    1.29  %