| changeset 17806 | b6a547bfb419 |
| parent 17780 | 274eaa114c6d |
| child 17809 | 195045659c06 |
--- 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)