# HG changeset patch
# User nipkow
# Date 869831955 -7200
# Node ID 04c6ae944b5e92de58298dfb2d6b35b3e7bef12d
# Parent  8bd9b4b3b61de943bb40c8be244eb691b6ad0e12
new simproc

diff -r 8bd9b4b3b61d -r 04c6ae944b5e NEWS
--- 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;