# HG changeset patch
# User wenzelm
# Date 949492017 -3600
# Node ID 6b7ef9fc39da959ebd2636f5035f275adb14591b
# Parent  344888de76c4a9ef3f4ff7e722877b84c422c52d
nat as names;
obtain;
tuned;

diff -r 344888de76c4 -r 6b7ef9fc39da NEWS
--- 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;