--- a/doc-src/Sledgehammer/sledgehammer.tex Sun Apr 22 14:16:46 2012 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Sun Apr 22 14:16:46 2012 +0200
@@ -95,7 +95,7 @@
and satisfiability-modulo-theories (SMT) solvers on the current goal.%
\footnote{The distinction between ATPs and SMT solvers is convenient but mostly
historical. The two communities are converging, with more and more ATPs
-supporting typical SMT features such as arithemtic and sorts, and a few SMT
+supporting typical SMT features such as arithmetic and sorts, and a few SMT
solvers parsing ATP syntaxes. There is also a strong technological connection
between instantiation-based ATPs (such as iProver and iProver-Eq) and SMT
solvers.}