# HG changeset patch
# User wenzelm
# Date 1591646166 -7200
# Node ID ebcae4a19e785bf2dcc8a18a9123b6a03035f806
# Parent  bee83c9d330664ada34f06534a98f2a986124669
NEWS;

diff -r bee83c9d3306 -r ebcae4a19e78 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).