--- a/NEWS Wed Feb 02 12:25:54 2000 +0100
+++ b/NEWS Wed Feb 02 12:46:57 2000 +0100
@@ -10,9 +10,17 @@
* HOL: the constant for f``x is now "image" rather than "op ``".
+*** Isar ***
+
+* names of theorems, assumptions etc. may be natural numbers as well;
+
+* new 'obtain' language element supports generalized existence proofs;
+
+
*** HOL ***
-* Algebra: new theory of rings and univariate polynomials, by Clemens Ballarin
+* Algebra: new theory of rings and univariate polynomials, by Clemens
+Ballarin;