Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
NEWS
changeset 81868 d832c4a676e1
parent 81813 8df58b532ecb
child 81892 f1d520cd7575
child 81960 326ecfc079a6 
--- a/NEWS	Fri Jan 17 21:30:08 2025 +0100
+++ b/NEWS	Fri Jan 17 22:38:15 2025 +0100
@@ -298,6 +298,9 @@
       image_mset_diff_if_inj
       minus_add_mset_if_not_in_lhs[simp]
 
+* Theory "HOL-Library.Suc_Notation" provides compact notation for nested
+Suc terms.
+
 * Transitional theory "HOL.Divides" moved to "HOL-Library.Divides" and
 supposed to be removed in a future release. Minor INCOMPATIBILITY.
 Import "HOL-Library.Divides" and keep an eye on qualified names with prefix
isabelle