--- 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"