1.1 --- a/NEWS	Fri May 14 23:16:33 2010 +0200
     1.2 +++ b/NEWS	Fri May 14 23:32:48 2010 +0200
     1.3 @@ -347,6 +347,24 @@
     1.4    Nat_Int_Bij.bij_nat_to_int_bij  ~> bij_int_encode
     1.5    Nat_Int_Bij.bij_int_to_nat_bij  ~> bij_int_decode
     1.6  
     1.7 +* Sledgehammer:
     1.8 +  - Renamed ATP commands:
     1.9 +    atp_info     ~> sledgehammer running_atps
    1.10 +    atp_kill     ~> sledgehammer kill_atps
    1.11 +    atp_messages ~> sledgehammer messages
    1.12 +    atp_minimize ~> sledgehammer minimize
    1.13 +    print_atps   ~> sledgehammer available_atps
    1.14 +    INCOMPATIBILITY.
    1.15 +  - Added user's manual ("isabelle doc sledgehammer").
    1.16 +  - Added option syntax and "sledgehammer_params" to customize
    1.17 +    Sledgehammer's behavior.  See the manual for details.
    1.18 +  - Modified the Isar proof reconstruction code so that it produces
    1.19 +    direct proofs rather than proofs by contradiction.  (This feature
    1.20 +    is still experimental.)
    1.21 +  - Made Isar proof reconstruction work for SPASS, remote ATPs, and in
    1.22 +    full-typed mode.
    1.23 +  - Added support for TPTP syntax for SPASS via the "spass_tptp" ATP.
    1.24 +
    1.25  * Nitpick:
    1.26    - Added and implemented "binary_ints" and "bits" options.
    1.27    - Added "std" option and implemented support for nonstandard models.