# HG changeset patch
# User wenzelm
# Date 1428749266 -7200
# Node ID 5fe58ca9cf40e0dd4f98864281e9cd813b77dbbf
# Parent  bd1c342dbbcede77876d04d40efa4bae7520ef60
tuned spelling;

diff -r bd1c342dbbce -r 5fe58ca9cf40 NEWS
--- a/NEWS	Sat Apr 11 12:40:03 2015 +0200
+++ b/NEWS	Sat Apr 11 12:47:46 2015 +0200
@@ -138,10 +138,10 @@
 * Command "class_deps" takes optional sort arguments to constrain then
 resulting class hierarchy.
 
-* Lexical separation of signed and unsigend numerals: categories "num"
-and "float" are unsigend.  INCOMPATIBILITY: subtle change in precedence
-of numeral signs, particulary in expressions involving infix syntax like
-"(- 1) ^ n".
+* Lexical separation of signed and unsigned numerals: categories "num"
+and "float" are unsigned. INCOMPATIBILITY: subtle change in precedence
+of numeral signs, particularly in expressions involving infix syntax
+like "(- 1) ^ n".
 
 * Old inner token category "xnum" has been discontinued.  Potential
 INCOMPATIBILITY for exotic syntax: may use mixfix grammar with "num"
@@ -207,7 +207,7 @@
     INCOMPATIBILITY.
 
 * Nitpick:
-  - Fixed soundness bug related to the strict and nonstrict subset
+  - Fixed soundness bug related to the strict and non-strict subset
     operations.
 
 * Sledgehammer:
@@ -216,7 +216,7 @@
   - Z3 is now always enabled by default, now that it is fully open
     source. The "z3_non_commercial" option is discontinued.
   - Minimization is now always enabled by default.
-    Removed subcommand:
+    Removed sub-command:
       min
   - Proof reconstruction, both one-liners and Isar, has been
     dramatically improved.
@@ -364,12 +364,12 @@
 * HOL-Decision_Procs: New counterexample generator quickcheck
 [approximation] for inequalities of transcendental functions. Uses
 hardware floating point arithmetic to randomly discover potential
-counterexamples. Counterexamples are certified with the 'approximation'
+counterexamples. Counterexamples are certified with the "approximation"
 method. See HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy for
 examples.
 
 * HOL-Probability: Reworked measurability prover
-  - applies destructor rules repeatetly
+  - applies destructor rules repeatedly
   - removed application splitting (replaced by destructor rule)
   - added congruence rules to rewrite measure spaces under the sets
     projection
@@ -384,7 +384,7 @@
 considered inaccessible, instead of accessible via the fully-qualified
 internal name. This mainly affects Name_Space.intern (and derivatives),
 which may produce an unexpected Long_Name.hidden prefix. Note that
-contempory applications use the strict Name_Space.check (and
+contemporary applications use the strict Name_Space.check (and
 derivatives) instead, which is not affected by the change. Potential
 INCOMPATIBILITY in rare applications of Name_Space.intern.