* Pure: removed obsolete 'exported' attribute;
authorwenzelm
Tue Oct 23 19:12:37 2001 +0200 (2001-10-23)
changeset 11899e543b0f01a58
parent 11898 0844573f4518
child 11900 f8f37d61fbc2
* 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");
NEWS
     1.1 --- a/NEWS	Mon Oct 22 23:39:00 2001 +0200
     1.2 +++ b/NEWS	Tue Oct 23 19:12:37 2001 +0200
     1.3 @@ -52,6 +52,12 @@
     1.4  
     1.5  * Pure: fixed 'token_translation' command;
     1.6  
     1.7 +* Pure: removed obsolete 'exported' attribute;
     1.8 +
     1.9 +* Pure: dummy pattern "_" in is/let is now automatically ``lifted''
    1.10 +over bound variables: "ALL x. P x --> Q x" (is "ALL x. _ --> ?C x")
    1.11 +supersedes more cumbersome ... (is "ALL x. _ x --> ?C x");
    1.12 +
    1.13  * HOL: 'typedef' now allows alternative names for Rep/Abs morphisms;
    1.14  
    1.15  * HOL: 'recdef' now fails on unfinished automated proofs, use