# 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)