NEWS
changeset 5275 de5d5e5eb692
parent 5267 41a01176b9de
child 5282 80c75c862a8f
--- a/NEWS	Thu Aug 06 12:48:21 1998 +0200
+++ b/NEWS	Thu Aug 06 12:52:03 1998 +0200
@@ -1,4 +1,3 @@
-
 Isabelle NEWS -- history of user-visible changes
 ================================================
 
@@ -14,6 +13,9 @@
 * HOL: renamed r^-1 to 'converse' from 'inverse'; `inj_onto' is now
 called `inj_on';
 
+* HOL: removed duplicate thms in Arith:
+  less_imp_add_less  should be replaced by  trans_less_add1
+  le_imp_add_le      should be replaced by  trans_le_add1
 
 *** Proof tools ***