NEWS
changeset 77267 1fde0e4fd791
parent 77137 79231a210f5d
child 77268 9653bea4aa83
--- a/NEWS	Tue Feb 14 08:10:17 2023 +0100
+++ b/NEWS	Tue Feb 14 09:36:06 2023 +0100
@@ -43,6 +43,8 @@
 
 *** HOL ***
 
+* Map.map_of and lemmas moved to List.
+
 * Theory "HOL.Euclidean_Division" renamed to "HOL.Euclidean_Rings";
   "euclidean division" typically denotes a particular division on
   integers.  Minor INCOMPATIBILITY.