Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
*** empty log message ***
authornipkow
Thu, 06 Aug 1998 12:52:03 +0200
changeset 5275 de5d5e5eb692
parent 5274 5a29c309b0b7
child 5276 dd99b958b306
*** empty log message ***
NEWS file | annotate | diff | comparison | revisions 
--- 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 ***
isabelle