NEWS
changeset 18979 f0873dcc880f
parent 18910 50a27d7c8951
child 19006 2427684c201c
equal deleted inserted replaced
18978:8971c306b94f 18979:f0873dcc880f
   305 * "LEAST x:A. P" expands to "LEAST x. x:A & P" (input only).
   305 * "LEAST x:A. P" expands to "LEAST x. x:A & P" (input only).
   306 
   306 
   307 * In the context of the assumption "~(s = t)" the Simplifier rewrites
   307 * In the context of the assumption "~(s = t)" the Simplifier rewrites
   308 "t = s" to False (by simproc "neq_simproc").  For backward
   308 "t = s" to False (by simproc "neq_simproc").  For backward
   309 compatibility this can be disabled by ML "reset use_neq_simproc".
   309 compatibility this can be disabled by ML "reset use_neq_simproc".
       
   310 
       
   311 * "m dvd n" where m and n are numbers is evaluated to True/False by simp.
   310 
   312 
   311 * Tactics 'sat' and 'satx' reimplemented, several improvements: goals
   313 * Tactics 'sat' and 'satx' reimplemented, several improvements: goals
   312 no longer need to be stated as "<prems> ==> False", equivalences (i.e.
   314 no longer need to be stated as "<prems> ==> False", equivalences (i.e.
   313 "=" on type bool) are handled, variable names of the form "lit_<n>"
   315 "=" on type bool) are handled, variable names of the form "lit_<n>"
   314 are no longer reserved, significant speedup.
   316 are no longer reserved, significant speedup.