* Pure: removed obsolete 'exported' attribute;
* Pure: dummy pattern "_" in is/let is now automatically ``lifted''
over bound variables: "ALL x. P x --> Q x" (is "ALL x. _ --> ?C x")
supersedes more cumbersome ... (is "ALL x. _ x --> ?C x");

--- a/NEWS	Mon Oct 22 23:39:00 2001 +0200
+++ b/NEWS	Tue Oct 23 19:12:37 2001 +0200
@@ -52,6 +52,12 @@
 
 * Pure: fixed 'token_translation' command;
 
+* Pure: removed obsolete 'exported' attribute;
+
+* Pure: dummy pattern "_" in is/let is now automatically ``lifted''
+over bound variables: "ALL x. P x --> Q x" (is "ALL x. _ --> ?C x")
+supersedes more cumbersome ... (is "ALL x. _ x --> ?C x");
+
 * HOL: 'typedef' now allows alternative names for Rep/Abs morphisms;
 
 * HOL: 'recdef' now fails on unfinished automated proofs, use