# HG changeset patch
# User wenzelm
# Date 1238774609 -7200
# Node ID 5106e13d400fa6af8afdc17cca9c645fd1f9edbc
# Parent  bfad8265dd34208fcd9f41c6f95c06b8066c535d
fixed formal markup;

diff -r bfad8265dd34 -r 5106e13d400f doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Apr 03 16:18:14 2009 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Apr 03 18:03:29 2009 +0200
@@ -768,7 +768,7 @@
   always supplied to the arithmetic provers implicitly.
 
   The @{attribute (HOL) arith_split} attribute declares case split
-  rules to be expanded before @{method_def (HOL) arith} is invoked.
+  rules to be expanded before @{method (HOL) arith} is invoked.
 
   Note that a simpler (but faster) arithmetic prover is
   already invoked by the Simplifier.
diff -r bfad8265dd34 -r 5106e13d400f doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Apr 03 16:18:14 2009 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Apr 03 18:03:29 2009 +0200
@@ -776,7 +776,7 @@
   always supplied to the arithmetic provers implicitly.
 
   The \hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isacharunderscore}split}}} attribute declares case split
-  rules to be expanded before \indexdef{HOL}{method}{arith}\hypertarget{method.HOL.arith}{\hyperlink{method.HOL.arith}{\mbox{\isa{arith}}}} is invoked.
+  rules to be expanded before \hyperlink{method.HOL.arith}{\mbox{\isa{arith}}} is invoked.
 
   Note that a simpler (but faster) arithmetic prover is
   already invoked by the Simplifier.%