new simproc

--- a/NEWS	Fri Jul 25 13:20:12 1997 +0200
+++ b/NEWS	Fri Jul 25 13:59:15 1997 +0200
@@ -5,6 +5,11 @@
 New in Isabelle???? (DATE ????)
 -------------------------------
 
+* HOL/simplifier: terms of the form
+  `? x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x)' (or t=x)
+  are rewritten to
+  `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t)'
+
 * HOL/Lists: the function "set_of_list" has been renamed "set"
 
 * removed old README and Makefiles;