NEWS
changeset 8184 6b7ef9fc39da
parent 8015 4a687092b201
child 8203 2fcc6017cb72
     1.1 --- a/NEWS	Wed Feb 02 12:25:54 2000 +0100
     1.2 +++ b/NEWS	Wed Feb 02 12:46:57 2000 +0100
     1.3 @@ -10,9 +10,17 @@
     1.4  * HOL: the constant for f``x is now "image" rather than "op ``".
     1.5  
     1.6  
     1.7 +*** Isar ***
     1.8 +
     1.9 +* names of theorems, assumptions etc. may be natural numbers as well;
    1.10 +
    1.11 +* new 'obtain' language element supports generalized existence proofs;
    1.12 +
    1.13 +
    1.14  *** HOL ***
    1.15  
    1.16 -* Algebra: new theory of rings and univariate polynomials, by Clemens Ballarin
    1.17 +* Algebra: new theory of rings and univariate polynomials, by Clemens
    1.18 +Ballarin;
    1.19  
    1.20  
    1.21