# HG changeset patch
# User wenzelm
# Date 1272890298 -7200
# Node ID af4d68eccf633612f778400207447afe0cb9459e
# Parent  b0c047d03208a920f033e7d1a0a6490d54801ee6
old NEWS on global operations;

diff -r b0c047d03208 -r af4d68eccf63 NEWS
--- a/NEWS	Mon May 03 14:31:33 2010 +0200
+++ b/NEWS	Mon May 03 14:38:18 2010 +0200
@@ -362,6 +362,12 @@
 * Configuration options now admit dynamic default values, depending on
 the context or even global references.
 
+* Most operations that refer to a global context are named
+accordingly, e.g. Simplifier.global_context or
+ProofContext.init_global.  There are some situations where a global
+context actually works, but under normal circumstances one needs to
+pass the proper local context through the code!
+
 
 *** System ***