NEWS;

--- a/NEWS	Mon Jun 08 21:55:14 2020 +0200
+++ b/NEWS	Mon Jun 08 21:56:06 2020 +0200
@@ -27,6 +27,9 @@
 
 *** HOL ***
 
+* Session HOL-Examples contains notable examples for Isabelle/HOL
+(former entries of HOL-Isar_Examples, HOL-ex etc.).
+
 * Simproc "datatype_no_proper_subterm" rewrites equalities "lhs = rhs"
 on datatypes to "False" if either side is a proper subexpression of the
 other (for any datatype with a reasonable size function).