--- a/NEWS Wed Oct 15 21:45:02 2008 +0200
+++ b/NEWS Wed Oct 15 22:12:02 2008 +0200
@@ -100,7 +100,8 @@
Posix processes. Avoids potentially expensive forking of the ML
process. New thread-based implementation also works on non-Unix
platforms (Cygwin). Provers are no longer hardwired, but defined
-within the theory via plain ML wrapper functions.
+within the theory via plain ML wrapper functions. Basic Sledgehammer
+commands are covered in the isar-ref manual
* Wrapper scripts for remote SystemOnTPTP service allows to use
sledgehammer without local ATP installation (Vampire etc.). See also