tuned;
authorwenzelm
Tue Jul 03 23:00:42 2007 +0200 (2007-07-03)
changeset 235626cad6b400cfd
parent 23561 a531c8da8a9b
child 23563 42f2f90b51a6
tuned;
NEWS
     1.1 --- a/NEWS	Tue Jul 03 22:27:30 2007 +0200
     1.2 +++ b/NEWS	Tue Jul 03 23:00:42 2007 +0200
     1.3 @@ -541,12 +541,14 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 -* Method "metis" proves goals by applying the Metis general-purpose resolution prover.
     1.8 -  Examples are in the directory MetisExamples.
     1.9 +* Method "metis" proves goals by applying the Metis general-purpose
    1.10 +resolution prover.  Examples are in the directory MetisExamples.  See
    1.11 +also http://gilith.com/software/metis/
    1.12    
    1.13 -* Command "sledgehammer" invokes external automatic theorem provers as background processes.
    1.14 -  It generates calls to the "metis" method if successful. These can be pasted into the proof.
    1.15 -  Users do not have to wait for the automatic provers to return.
    1.16 +* Command 'sledgehammer' invokes external automatic theorem provers as
    1.17 +background processes.  It generates calls to the "metis" method if
    1.18 +successful. These can be pasted into the proof.  Users do not have to
    1.19 +wait for the automatic provers to return.
    1.20  
    1.21  * IntDef: The constant "int :: nat => int" has been removed; now "int"
    1.22    is an abbreviation for "of_nat :: nat => int". The simplification rules