NEWS
changeset 16104 dab13c4685ba
parent 16102 c5f6726d9bb1
child 16111 d06dc7975731
--- a/NEWS	Fri May 27 16:33:33 2005 +0200
+++ b/NEWS	Fri May 27 17:10:23 2005 +0200
@@ -78,7 +78,7 @@
 
 * Pure: print_tac now outputs the goal through the trace channel.
 
-* Pure: reference Namespace.unique_names included.  If true the
+* Pure: reference NameSpace.unique_names included.  If true the
   (shortest) namespace-prefix is printed to disambiguate conflicts (as
   yet). If false the first entry wins (as during parsing). Default
   value is true.