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