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.
more NEWS;
authorwenzelm
Fri, 17 Jan 2025 22:38:15 +0100
changeset 81868 d832c4a676e1
parent 81867 f0ae2acbefd5
child 81869 24ef42cab7d6
more NEWS;
NEWS file | annotate | diff | comparison | revisions 
--- 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