equal
deleted
inserted
replaced
774 |
774 |
775 The \hyperlink{attribute.HOL.arith}{\mbox{\isa{arith}}} attribute declares facts that are |
775 The \hyperlink{attribute.HOL.arith}{\mbox{\isa{arith}}} attribute declares facts that are |
776 always supplied to the arithmetic provers implicitly. |
776 always supplied to the arithmetic provers implicitly. |
777 |
777 |
778 The \hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isacharunderscore}split}}} attribute declares case split |
778 The \hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isacharunderscore}split}}} attribute declares case split |
779 rules to be expanded before \indexdef{HOL}{method}{arith}\hypertarget{method.HOL.arith}{\hyperlink{method.HOL.arith}{\mbox{\isa{arith}}}} is invoked. |
779 rules to be expanded before \hyperlink{method.HOL.arith}{\mbox{\isa{arith}}} is invoked. |
780 |
780 |
781 Note that a simpler (but faster) arithmetic prover is |
781 Note that a simpler (but faster) arithmetic prover is |
782 already invoked by the Simplifier.% |
782 already invoked by the Simplifier.% |
783 \end{isamarkuptext}% |
783 \end{isamarkuptext}% |
784 \isamarkuptrue% |
784 \isamarkuptrue% |