--- 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