diff -r a053f13bc9da -r f131f0fbf9cd NEWS
--- a/NEWS	Mon Apr 14 22:29:56 2008 +0200
+++ b/NEWS	Tue Apr 15 16:11:52 2008 +0200
@@ -26,20 +26,31 @@
 file are no longer supported.  INCOMPATIBILITY, regular 'uses' and
 'use' within a theory file will do the job.
 
+* Name space merge now observes canonical order, i.e. the second space
+is inserted into the first one, while existing entries in the first
+space take precedence.  INCOMPATIBILITY is rare situations, may try to
+swap theory imports.
+
 
 *** Pure ***
 
+* Authentic naming of facts disallows ad-hoc overwriting of previous
+theorems within the same name space.  INCOMPATIBILITY, need to remove
+duplicate fact bindings, or even accidental fact duplications.  Note
+that tools may maintain dynamically scoped facts systematically, using
+PureThy.add_thms_dynamic.
+
 * Eliminated destructive theorem database, simpset, claset, and
 clasimpset.  Potential INCOMPATIBILITY, really need to observe linear
 update of theories within ML code.
 
+* Eliminated theory ProtoPure.  Potential INCOMPATIBILITY.
+
 * Commands 'use' and 'ML' are now purely functional, operating on
 theory/local_theory.  Removed former 'ML_setup' (on theory), use 'ML'
 instead.  Added 'ML_val' as mere diagnostic replacement for 'ML'.
 INCOMPATIBILITY.
 
-* Eliminated theory ProtoPure.  Potential INCOMPATIBILITY.
-
 * Command 'setup': discontinued implicit version.
 
 * Instantiation target allows for simultaneous specification of class