# HG changeset patch
# User wenzelm
# Date 936014917 -7200
# Node ID f819265e267c2f9357383285b2f07efce9bf8c5c
# Parent  f647f463abebfd1d94568dc82d20a607ecbab40c
'arith' method;

diff -r f647f463abeb -r f819265e267c doc-src/IsarRef/hol.tex
--- a/doc-src/IsarRef/hol.tex	Mon Aug 30 14:08:23 1999 +0200
+++ b/doc-src/IsarRef/hol.tex	Mon Aug 30 14:08:37 1999 +0200
@@ -182,6 +182,18 @@
 \end{descr}
 
 
+\section{Arithmetic}
+
+\indexisarmeth{arith}
+\begin{matharray}{rcl}
+  arith & : & \isarmeth \\
+\end{matharray}
+
+The $arith$ method decides linear arithmetic problems (on types $nat$, $int$,
+$real$).  Note that a simpler (but faster) version of arithmetic reasoning is
+already performed by the Simplifier.
+
+
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "isar-ref"