# HG changeset patch
# User nipkow
# Date 1128807361 -7200
# Node ID b6a547bfb41909d2dcf843097ef8d9c527e8c7f9
# Parent  a9c2d42937ddb63ec483e6dcd96686bc94519586
*** empty log message ***

diff -r a9c2d42937dd -r b6a547bfb419 NEWS
--- a/NEWS	Sat Oct 08 23:05:59 2005 +0200
+++ b/NEWS	Sat Oct 08 23:36:01 2005 +0200
@@ -22,6 +22,11 @@
 translation.  INCOMPATIBILITY -- use dummy abstraction instead, for
 example "A -> B" => "Pi A (%_. B)".
 
+*** HOL ***
+
+* In the context of the assumption "~(s = t)" the simplifier rewrites
+"t = s" to False (by simproc "neq_simproc"). For backward compatibility
+this can be disabled by ML"reset use_neq_simproc".
 
 
 New in Isabelle2005 (October 2005)