* Pure/Namespace: flag unique_names added
* Pure/Tactic: print_tac outputs goal through trace channel
* HOL/Simplifier: extended record_upd_simproc

--- a/NEWS	Tue Jul 06 20:32:20 2004 +0200
+++ b/NEWS	Tue Jul 06 20:34:49 2004 +0200
@@ -42,6 +42,14 @@
   'nonterminals' rather than 'types'.  INCOMPATIBILITY for new
   object-logic specifications.
 
+* Pure/Tactic: print_tac now outputs the goal through the trace 
+  channel.
+
+* Pure/Namespace: 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.
+
 * Pure/Syntax: inner syntax includes (*(*nested*) comments*).
 
 * Pure/Syntax: pretty pinter now supports unbreakable blocks,
@@ -96,9 +104,9 @@
   the old record representation. The type generated for a record is
   called <record_name>_ext_type.
 
-* HOL/record: Reference record_definition_quick_and_dirty_sensitive
+* HOL/record: Reference record_quick_and_dirty_sensitive
   can be enabled to skip the proofs triggered by a record definition
-  (if quick_and_dirty is enabled). Definitions of large records can
+  or a simproc (if quick_and_dirty is enabled). Definitions of large records can
   take quite long.
 
 * HOL: symbolic syntax of Hilbert Choice Operator is now as follows:
@@ -112,9 +120,10 @@
   \<epsilon> becomes available as variable, constant etc.
 
 * Simplifier: "record_upd_simproc" for simplification of multiple
-  record updates enabled by default.  INCOMPATIBILITY: old proofs
-  break occasionally, since simplification is more powerful by
-  default.
+  record updates enabled by default. Moreover trivial updates are
+  also removed: r(|x := x r|) = r. 
+  INCOMPATIBILITY: old proofs break occasionally, since simplification 
+  is more powerful by default.
 
 
 *** HOLCF ***