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 ***