updated NEWS
authorimmler@in.tum.de
Sat Mar 14 17:52:53 2009 +0100 (2009-03-14)
changeset 30538a77b7995062a
parent 30537 0dd8dfe424cf
child 30539 c96c72709a20
updated NEWS
NEWS
     1.1 --- a/NEWS	Sat Mar 14 16:50:25 2009 +0100
     1.2 +++ b/NEWS	Sat Mar 14 17:52:53 2009 +0100
     1.3 @@ -335,10 +335,9 @@
     1.4  commands are covered in the isar-ref manual.
     1.5  
     1.6  * Wrapper scripts for remote SystemOnTPTP service allows to use
     1.7 -sledgehammer without local ATP installation (Vampire etc.).  See also
     1.8 -ISABELLE_HOME/contrib/SystemOnTPTP and the VAMPIRE_HOME setting
     1.9 -variable.  Other provers may be included via suitable ML wrappers, see
    1.10 -also src/HOL/ATP_Linkup.thy.
    1.11 +sledgehammer without local ATP installation (Vampire etc.). Other
    1.12 +provers may be included via suitable ML wrappers, see also
    1.13 +src/HOL/ATP_Linkup.thy.
    1.14  
    1.15  * Normalization by evaluation now allows non-leftlinear equations.
    1.16  Declare with attribute [code nbe].