--- a/NEWS Sat Oct 08 23:43:15 2005 +0200
+++ b/NEWS Sun Oct 09 17:06:03 2005 +0200
@@ -28,6 +28,11 @@
"t = s" to False (by simproc "neq_simproc"). For backward compatibility
this can be disabled by ML"reset use_neq_simproc".
+* 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>" are
+no longer reserved, significant speedup.
+
New in Isabelle2005 (October 2005)
----------------------------------