simplification procedure unit_eq_proc rewrites (?x::unit) = ();
quote / antiquote translations;

--- a/NEWS	Thu Jun 25 15:37:36 1998 +0200
+++ b/NEWS	Thu Jun 25 16:12:02 1998 +0200
@@ -49,6 +49,11 @@
 * HOL/record: now includes concrete syntax for record terms (still
 lacks important theorems, like surjective pairing and split);
 
+* simplification procedure unit_eq_proc rewrites (?x::unit) = (); this
+is made part of the default simpset of Prod.thy, which COULD MAKE
+EXISTING PROOFS FAIL (consider 'Delsimprocs [unit_eq_proc];' as last
+resort);
+
 * new force_tac (and its derivations Force_tac, force): combines
 rewriting and classical reasoning (and whatever other tools) similarly
 to auto_tac, but is aimed to solve the given subgoal totally;
@@ -124,6 +129,9 @@
 kind name replaced by private Object.kind, acting as authorization
 key); new type-safe user interface via functor TheoryDataFun;
 
+* module Pure/Syntax now offers quote / antiquote translation
+functions (useful for Hoare logic etc. with implicit dependencies);
+
 
 
 New in Isabelle98 (January 1998)