1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Apr 03 16:18:14 2009 +0200
1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Apr 03 18:03:29 2009 +0200
1.3 @@ -768,7 +768,7 @@
1.4 always supplied to the arithmetic provers implicitly.
1.5
1.6 The @{attribute (HOL) arith_split} attribute declares case split
1.7 - rules to be expanded before @{method_def (HOL) arith} is invoked.
1.8 + rules to be expanded before @{method (HOL) arith} is invoked.
1.9
1.10 Note that a simpler (but faster) arithmetic prover is
1.11 already invoked by the Simplifier.
2.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Apr 03 16:18:14 2009 +0200
2.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Apr 03 18:03:29 2009 +0200
2.3 @@ -776,7 +776,7 @@
2.4 always supplied to the arithmetic provers implicitly.
2.5
2.6 The \hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isacharunderscore}split}}} attribute declares case split
2.7 - rules to be expanded before \indexdef{HOL}{method}{arith}\hypertarget{method.HOL.arith}{\hyperlink{method.HOL.arith}{\mbox{\isa{arith}}}} is invoked.
2.8 + rules to be expanded before \hyperlink{method.HOL.arith}{\mbox{\isa{arith}}} is invoked.
2.9
2.10 Note that a simpler (but faster) arithmetic prover is
2.11 already invoked by the Simplifier.%