fixed typos
authorblanchet
Sun Apr 22 14:16:46 2012 +0200 (2012-04-22)
changeset 476721bf4fa90cd03
parent 47671 ab44addc81e2
child 47673 dd253cfa5b23
child 47675 4483c004499a
fixed typos
NEWS
doc-src/Sledgehammer/sledgehammer.tex
     1.1 --- a/NEWS	Sun Apr 22 14:16:46 2012 +0200
     1.2 +++ b/NEWS	Sun Apr 22 14:16:46 2012 +0200
     1.3 @@ -5275,7 +5275,7 @@
     1.4  * HOL/Nat: neq0_conv no longer declared as iff.  INCOMPATIBILITY.
     1.5  
     1.6  * HOL-Word: New extensive library and type for generic, fixed size
     1.7 -machine words, with arithemtic, bit-wise, shifting and rotating
     1.8 +machine words, with arithmetic, bit-wise, shifting and rotating
     1.9  operations, reflection into int, nat, and bool lists, automation for
    1.10  linear arithmetic (by automatic reflection into nat or int), including
    1.11  lemmas on overflow and monotonicity.  Instantiated to all appropriate
     2.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Sun Apr 22 14:16:46 2012 +0200
     2.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Sun Apr 22 14:16:46 2012 +0200
     2.3 @@ -95,7 +95,7 @@
     2.4  and satisfiability-modulo-theories (SMT) solvers on the current goal.%
     2.5  \footnote{The distinction between ATPs and SMT solvers is convenient but mostly
     2.6  historical. The two communities are converging, with more and more ATPs
     2.7 -supporting typical SMT features such as arithemtic and sorts, and a few SMT
     2.8 +supporting typical SMT features such as arithmetic and sorts, and a few SMT
     2.9  solvers parsing ATP syntaxes. There is also a strong technological connection
    2.10  between instantiation-based ATPs (such as iProver and iProver-Eq) and SMT
    2.11  solvers.}