1.1 --- a/CONTRIBUTORS	Mon Sep 12 10:49:37 2011 +0200
     1.2 +++ b/CONTRIBUTORS	Mon Sep 12 11:05:32 2011 +0200
     1.3 @@ -16,6 +16,11 @@
     1.4    Various building blocks for Isabelle/Scala layer and Isabelle/jEdit
     1.5    Prover IDE.
     1.6  
     1.7 +* 2011: Jasmin Blanchette, TUM
     1.8 +  Various improvements to Sledgehammer, notably: use of sound translations,
     1.9 +  support for more provers (Waldmeister, LEO-II, Satallax). Further development
    1.10 +  of Nitpick and "try".
    1.11 +
    1.12  
    1.13  Contributions to Isabelle2011
    1.14  -----------------------------

     2.1 --- a/NEWS	Mon Sep 12 10:49:37 2011 +0200
     2.2 +++ b/NEWS	Mon Sep 12 11:05:32 2011 +0200
     2.3 @@ -180,10 +180,13 @@
     2.4      INCOMPATIBILITY.
     2.5  
     2.6  * Sledgehammer:
     2.7 +  - Use quasi-sound (and efficient) translations by default.
     2.8 +  - Added support for the following provers: E-ToFoF, LEO-II, Satallax, SNARK,
     2.9 +    Waldmeister, and Z3 with TPTP syntax.
    2.10 +  - Automatically preplay and minimize proofs before showing them if this can be
    2.11 +    done within reasonable time.
    2.12    - sledgehammer available_provers ~> sledgehammer supported_provers.
    2.13      INCOMPATIBILITY.
    2.14 -  - Added support for SNARK and ToFoF-E on SystemOnTPTP and for simply typed
    2.15 -    TPTP problems (TFF).
    2.16    - Added "preplay_timeout", "slicing", "type_enc", "sound", "max_mono_iters",
    2.17      and "max_new_mono_instances" options.
    2.18    - Removed "explicit_apply" and "full_types" options as well as "Full Types"
    2.19 @@ -196,7 +199,7 @@
    2.20  * Command 'try':
    2.21    - Renamed 'try_methods' and added "simp:", "intro:", "dest:", and
    2.22      "elim:" options. INCOMPATIBILITY.
    2.23 -  - Introduced 'tryÄ that not only runs 'try_methods' but also
    2.24 +  - Introduced 'try' that not only runs 'try_methods' but also
    2.25      'solve_direct', 'sledgehammer', 'quickcheck', and 'nitpick'.
    2.26  
    2.27  * Quickcheck: