# HG changeset patch
# User wenzelm
# Date 1003857157 -7200
# Node ID e543b0f01a58f5ec089e4eb8fc6853860e1eef5e
# Parent  0844573f4518cf0b003a57b7468c42416a2ef8f3
* 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");

diff -r 0844573f4518 -r e543b0f01a58 NEWS
--- 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