doc-src/Sledgehammer/sledgehammer.tex
changeset 47672 1bf4fa90cd03
parent 47642 9a9218111085
child 47963 46c73ad5f7c0
     1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Sun Apr 22 14:16:46 2012 +0200
     1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Sun Apr 22 14:16:46 2012 +0200
     1.3 @@ -95,7 +95,7 @@
     1.4  and satisfiability-modulo-theories (SMT) solvers on the current goal.%
     1.5  \footnote{The distinction between ATPs and SMT solvers is convenient but mostly
     1.6  historical. The two communities are converging, with more and more ATPs
     1.7 -supporting typical SMT features such as arithemtic and sorts, and a few SMT
     1.8 +supporting typical SMT features such as arithmetic and sorts, and a few SMT
     1.9  solvers parsing ATP syntaxes. There is also a strong technological connection
    1.10  between instantiation-based ATPs (such as iProver and iProver-Eq) and SMT
    1.11  solvers.}