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