1.1 --- a/CONTRIBUTORS	Wed Apr 18 22:40:25 2012 +0200
     1.2 +++ b/CONTRIBUTORS	Wed Apr 18 22:40:25 2012 +0200
     1.3 @@ -17,9 +17,13 @@
     1.4    Alexander Krauss, QAware GmbH
     1.5    Faster and more scalable Import mechanism for HOL Light proofs.
     1.6  
     1.7 -* January 2012: Florian Haftmann, TUM, et. al.
     1.8 +* January 2012: Florian Haftmann, TUM, et al.
     1.9    (Re-)Introduction of the "set" type constructor.
    1.10  
    1.11 +* 2011/2012: Jasmin Blanchette, TUM
    1.12 +  Various improvements to Sledgehammer, notably: tighter integration
    1.13 +  with SPASS, support for more provers (Alt-Ergo, iProver, iProver-Eq).
    1.14 +
    1.15  * 2011/2012: Makarius Wenzel, Université Paris-Sud / LRI
    1.16    Various refinements of local theory infrastructure.
    1.17    Improvements of Isabelle/Scala layer and Isabelle/jEdit Prover IDE.

     2.1 --- a/NEWS	Wed Apr 18 22:40:25 2012 +0200
     2.2 +++ b/NEWS	Wed Apr 18 22:40:25 2012 +0200
     2.3 @@ -617,11 +617,17 @@
     2.4      conjectures in a locale context.
     2.5  
     2.6  * Nitpick:
     2.7 -
     2.8    - Fixed infinite loop caused by the 'peephole_optim' option and
     2.9      affecting 'rat' and 'real'.
    2.10  
    2.11  * Sledgehammer:
    2.12 +  - Integrated more tightly with SPASS, as described in the ITP 2012 paper "More
    2.13 +    SPASS with Isabelle".
    2.14 +  - Made it try "smt" as a fallback if "metis" fails or times out.
    2.15 +  - Added support for the following provers: Alt-Ergo (via Why3 and TFF1),
    2.16 +    iProver, iProver-Eq.
    2.17 +  - Replaced remote E-SInE with remote Satallax in the default setup.
    2.18 +  - Sped up the minimizer.
    2.19    - Added "lam_trans", "uncurry_aliases", and "minimize" options.
    2.20    - Renamed "slicing" ("no_slicing") option to "slice" ("dont_slice").
    2.21    - Renamed "sound" option to "strict".
    2.22 @@ -631,7 +637,7 @@
    2.23      parenthesized argument (e.g., "by (metis (lifting) ...)").
    2.24  
    2.25  * SMT:
    2.26 -  - renamed "smt_fixed" option to "smt_read_only_certificates".
    2.27 +  - Renamed "smt_fixed" option to "smt_read_only_certificates".
    2.28  
    2.29  * Command 'try0':
    2.30    - Renamed from 'try_methods'. INCOMPATIBILITY.