1.1 --- a/NEWS	Mon Dec 06 13:34:05 2010 -0800
     1.2 +++ b/NEWS	Mon Dec 06 13:43:05 2010 -0800
     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]]
    1.21 @@ -334,8 +334,8 @@
    1.22  of euclidean spaces the real and complex numbers are instantiated to
    1.23  be euclidean_spaces.  INCOMPATIBILITY.
    1.24  
    1.25 -* Probability: Introduced pinfreal as real numbers with infinity. Use
    1.26 -pinfreal as value for measures. Introduce the Radon-Nikodym
    1.27 +* Probability: Introduced pextreal as positive extended real numbers.
    1.28 +Use pextreal as value for measures. Introduce the Radon-Nikodym
    1.29  derivative, product spaces and Fubini's theorem for arbitrary sigma
    1.30  finite measures. Introduces Lebesgue measure based on the integral in
    1.31  Multivariate Analysis.  INCOMPATIBILITY.
    1.32 @@ -652,6 +652,9 @@
    1.33  
    1.34  *** System ***
    1.35  
    1.36 +* The IsabelleText font now includes Cyrillic, Hebrew, Arabic from
    1.37 +DajaVu Sans.
    1.38 +
    1.39  * Discontinued support for Poly/ML 5.0 and 5.1 versions.
    1.40  
    1.41