# HG changeset patch
# User wenzelm
# Date 1183496442 -7200
# Node ID 6cad6b400cfd49e9f2c65d6c9839401b1515f042
# Parent  a531c8da8a9b810fc7330b7c19c5910cb3592ee1
tuned;

diff -r a531c8da8a9b -r 6cad6b400cfd NEWS
--- a/NEWS	Tue Jul 03 22:27:30 2007 +0200
+++ b/NEWS	Tue Jul 03 23:00:42 2007 +0200
@@ -541,12 +541,14 @@
 
 *** HOL ***
 
-* Method "metis" proves goals by applying the Metis general-purpose resolution prover.
-  Examples are in the directory MetisExamples.
+* Method "metis" proves goals by applying the Metis general-purpose
+resolution prover.  Examples are in the directory MetisExamples.  See
+also http://gilith.com/software/metis/
   
-* Command "sledgehammer" invokes external automatic theorem provers as background processes.
-  It generates calls to the "metis" method if successful. These can be pasted into the proof.
-  Users do not have to wait for the automatic provers to return.
+* Command 'sledgehammer' invokes external automatic theorem provers as
+background processes.  It generates calls to the "metis" method if
+successful. These can be pasted into the proof.  Users do not have to
+wait for the automatic provers to return.
 
 * IntDef: The constant "int :: nat => int" has been removed; now "int"
   is an abbreviation for "of_nat :: nat => int". The simplification rules