--- 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.
--- 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},
--- 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 {*