# HG changeset patch
# User blanchet
# Date 1402588249 -7200
# Node ID 62746a41cc0c7003b2c77adca0d272b78395ff1a
# Parent  f6bf6d5341ee443b2eac32309e97e3fda0464f89
tuning

diff -r f6bf6d5341ee -r 62746a41cc0c NEWS
--- a/NEWS	Thu Jun 12 17:10:12 2014 +0200
+++ b/NEWS	Thu Jun 12 17:50:49 2014 +0200
@@ -387,7 +387,7 @@
     SMT-LIB 2 and quantifiers.
 
 * Sledgehammer:
-  - "z3" can now produce Isar proofs
+  - Z3 can now produce Isar proofs.
   - MaSh overhaul:
       - New SML-based learning engines eliminate the dependency on Python
         and increase performance and reliability.
diff -r f6bf6d5341ee -r 62746a41cc0c src/Doc/manual.bib
--- a/src/Doc/manual.bib	Thu Jun 12 17:10:12 2014 +0200
+++ b/src/Doc/manual.bib	Thu Jun 12 17:50:49 2014 +0200
@@ -204,7 +204,6 @@
                Cesare Tinelli},
   title     = {{CVC4}},
   booktitle = {CAV 2011},
-  year      = {2011},
   pages     = {171--177},
   editor    = {Ganesh Gopalakrishnan and
                Shaz Qadeer},
diff -r f6bf6d5341ee -r 62746a41cc0c src/HOL/SMT2.thy
--- a/src/HOL/SMT2.thy	Thu Jun 12 17:10:12 2014 +0200
+++ b/src/HOL/SMT2.thy	Thu Jun 12 17:50:49 2014 +0200
@@ -200,6 +200,7 @@
 *}
 
 declare [[cvc3_new_options = ""]]
+declare [[cvc4_new_options = ""]]
 declare [[z3_new_options = ""]]
 
 text {*