# HG changeset patch
# User nipkow
# Date 1139408274 -3600
# Node ID f0873dcc880f13eacd3cc98c3704a327cba9bbf3
# Parent  8971c306b94f87cd05b0f267454d730f0553708e
*** empty log message ***

diff -r 8971c306b94f -r f0873dcc880f NEWS
--- a/NEWS	Wed Feb 08 15:12:59 2006 +0100
+++ b/NEWS	Wed Feb 08 15:17:54 2006 +0100
@@ -308,6 +308,8 @@
 "t = s" to False (by simproc "neq_simproc").  For backward
 compatibility this can be disabled by ML "reset use_neq_simproc".
 
+* "m dvd n" where m and n are numbers is evaluated to True/False by simp.
+
 * Tactics 'sat' and 'satx' reimplemented, several improvements: goals
 no longer need to be stated as "<prems> ==> False", equivalences (i.e.
 "=" on type bool) are handled, variable names of the form "lit_<n>"