# HG changeset patch
# User blanchet
# Date 1335097006 -7200
# Node ID 1bf4fa90cd037e0360c642e1132a632a71c25715
# Parent  ab44addc81e28eb66f22c8d4bb27e76cb2504ec6
fixed typos

diff -r ab44addc81e2 -r 1bf4fa90cd03 NEWS
--- a/NEWS	Sun Apr 22 14:16:46 2012 +0200
+++ b/NEWS	Sun Apr 22 14:16:46 2012 +0200
@@ -5275,7 +5275,7 @@
 * HOL/Nat: neq0_conv no longer declared as iff.  INCOMPATIBILITY.
 
 * HOL-Word: New extensive library and type for generic, fixed size
-machine words, with arithemtic, bit-wise, shifting and rotating
+machine words, with arithmetic, bit-wise, shifting and rotating
 operations, reflection into int, nat, and bool lists, automation for
 linear arithmetic (by automatic reflection into nat or int), including
 lemmas on overflow and monotonicity.  Instantiated to all appropriate
diff -r ab44addc81e2 -r 1bf4fa90cd03 doc-src/Sledgehammer/sledgehammer.tex
--- 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.}