*** empty log message ***
authornipkow
Thu Aug 06 12:52:03 1998 +0200 (1998-08-06)
changeset 5275de5d5e5eb692
parent 5274 5a29c309b0b7
child 5276 dd99b958b306
*** empty log message ***
NEWS
     1.1 --- a/NEWS	Thu Aug 06 12:48:21 1998 +0200
     1.2 +++ b/NEWS	Thu Aug 06 12:52:03 1998 +0200
     1.3 @@ -1,4 +1,3 @@
     1.4 -
     1.5  Isabelle NEWS -- history of user-visible changes
     1.6  ================================================
     1.7  
     1.8 @@ -14,6 +13,9 @@
     1.9  * HOL: renamed r^-1 to 'converse' from 'inverse'; `inj_onto' is now
    1.10  called `inj_on';
    1.11  
    1.12 +* HOL: removed duplicate thms in Arith:
    1.13 +  less_imp_add_less  should be replaced by  trans_less_add1
    1.14 +  le_imp_add_le      should be replaced by  trans_le_add1
    1.15  
    1.16  *** Proof tools ***
    1.17