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 ***