fixed formal markup;
authorwenzelm
Fri Apr 03 18:03:29 2009 +0200 (2009-04-03)
changeset 308655106e13d400f
parent 30864 bfad8265dd34
child 30866 dd5117e2d73e
child 30870 61f2131554cd
child 30874 34927a1e0ae8
fixed formal markup;
doc-src/IsarRef/Thy/HOL_Specific.thy
doc-src/IsarRef/Thy/document/HOL_Specific.tex
     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.%