# HG changeset patch
# User wenzelm
# Date 1441539438 -7200
# Node ID a39e9c46a7722e193bfaa4525bd51ba97626a2e0
# Parent  4b5872b9d7832f0a0c46a346893eb7d162ea8175
NEWS;

diff -r 4b5872b9d783 -r a39e9c46a772 NEWS
--- a/NEWS	Fri Sep 04 22:16:54 2015 +0200
+++ b/NEWS	Sun Sep 06 13:37:18 2015 +0200
@@ -181,6 +181,12 @@
 
 *** HOL ***
 
+* Qualification of various formal entities in the libraries is done more
+uniformly via "context begin qualified definition ... end" instead of
+old-style "hide_const (open) ...". Consequently, both the defined
+constant and its defining fact become qualified, e.g. Option.is_none and
+Option.is_none_def. Occasional INCOMPATIBILITY in applications.
+
 * Some old and rarely used ASCII replacement syntax has been removed.
 INCOMPATIBILITY, standard syntax with symbols should be used instead.
 The subsequent commands help to reproduce the old forms, e.g. to