more correct NEWS;
authorwenzelm
Mon Dec 06 16:37:15 2010 +0100 (2010-12-06)
changeset 41020f1e9db633212
parent 41019 b63cb15e96aa
child 41021 3efa0ec42ed4
more correct NEWS;
NEWS
     1.1 --- a/NEWS	Mon Dec 06 16:18:56 2010 +0100
     1.2 +++ b/NEWS	Mon Dec 06 16:37:15 2010 +0100
     1.3 @@ -84,7 +84,7 @@
     1.4  *** Pure ***
     1.5  
     1.6  * Command 'notepad' replaces former 'example_proof' for
     1.7 -experimentation in Isar without and result.  INCOMPATIBILITY.
     1.8 +experimentation in Isar without any result.  INCOMPATIBILITY.
     1.9  
    1.10  * Support for real valued preferences (with approximative PGIP type).
    1.11  
    1.12 @@ -133,7 +133,7 @@
    1.13  
    1.14  Currently coercion inference is activated only in theories including
    1.15  real numbers, i.e. descendants of Complex_Main.  This is controlled by
    1.16 -the configuration option "infer_coercions", e.g. it can be enabled in
    1.17 +the configuration option "coercion_enabled", e.g. it can be enabled in
    1.18  other theories like this:
    1.19  
    1.20    declare [[coercion_enabled]]