# HG changeset patch
# User wenzelm
# Date 1291649835 -3600
# Node ID f1e9db633212ea668163707db57d978a39987528
# Parent  b63cb15e96aa271bd8b74d7a706d0c8f8dd5d8fb
more correct NEWS;

diff -r b63cb15e96aa -r f1e9db633212 NEWS
--- a/NEWS	Mon Dec 06 16:18:56 2010 +0100
+++ b/NEWS	Mon Dec 06 16:37:15 2010 +0100
@@ -84,7 +84,7 @@
 *** Pure ***
 
 * Command 'notepad' replaces former 'example_proof' for
-experimentation in Isar without and result.  INCOMPATIBILITY.
+experimentation in Isar without any result.  INCOMPATIBILITY.
 
 * Support for real valued preferences (with approximative PGIP type).
 
@@ -133,7 +133,7 @@
 
 Currently coercion inference is activated only in theories including
 real numbers, i.e. descendants of Complex_Main.  This is controlled by
-the configuration option "infer_coercions", e.g. it can be enabled in
+the configuration option "coercion_enabled", e.g. it can be enabled in
 other theories like this:
 
   declare [[coercion_enabled]]