NEWS
changeset 8283 0a319c5746eb
parent 8271 7602b57ba028
child 8358 a57d72b5d272
     1.1 --- a/NEWS	Tue Feb 22 21:51:25 2000 +0100
     1.2 +++ b/NEWS	Tue Feb 22 21:53:17 2000 +0100
     1.3 @@ -16,8 +16,19 @@
     1.4  
     1.5  * intro/elim/dest attributes: changed ! / !! flags to ? / ??;
     1.6  
     1.7 +* Pure now provides its own version of intro/elim/dest attributes;
     1.8 +useful for building new logics, but beware of confusion with the
     1.9 +Provers/classical ones!
    1.10 +
    1.11  * new 'obtain' language element supports generalized existence proofs;
    1.12  
    1.13 +* HOL: removed "case_split" thm binding, should use "cases" proof
    1.14 +method anyway;
    1.15 +
    1.16 +* tuned syntax of "induct" method;
    1.17 +
    1.18 +* new "cases" method for propositions, inductive sets and types;
    1.19 +
    1.20  
    1.21  *** HOL ***
    1.22  
    1.23 @@ -25,7 +36,7 @@
    1.24  Ballarin;
    1.25  
    1.26  * HOL/record: fixed select-update simplification procedure to handle
    1.27 -extended records as well;
    1.28 +extended records as well; admit "r" as field name;
    1.29  
    1.30  
    1.31