tuning
authorblanchet
Thu Jun 12 17:50:49 2014 +0200 (2014-06-12)
changeset 5724662746a41cc0c
parent 57245 f6bf6d5341ee
child 57248 5496011859eb
tuning
NEWS
src/Doc/manual.bib
src/HOL/SMT2.thy
     1.1 --- a/NEWS	Thu Jun 12 17:10:12 2014 +0200
     1.2 +++ b/NEWS	Thu Jun 12 17:50:49 2014 +0200
     1.3 @@ -387,7 +387,7 @@
     1.4      SMT-LIB 2 and quantifiers.
     1.5  
     1.6  * Sledgehammer:
     1.7 -  - "z3" can now produce Isar proofs
     1.8 +  - Z3 can now produce Isar proofs.
     1.9    - MaSh overhaul:
    1.10        - New SML-based learning engines eliminate the dependency on Python
    1.11          and increase performance and reliability.
     2.1 --- a/src/Doc/manual.bib	Thu Jun 12 17:10:12 2014 +0200
     2.2 +++ b/src/Doc/manual.bib	Thu Jun 12 17:50:49 2014 +0200
     2.3 @@ -204,7 +204,6 @@
     2.4                 Cesare Tinelli},
     2.5    title     = {{CVC4}},
     2.6    booktitle = {CAV 2011},
     2.7 -  year      = {2011},
     2.8    pages     = {171--177},
     2.9    editor    = {Ganesh Gopalakrishnan and
    2.10                 Shaz Qadeer},
     3.1 --- a/src/HOL/SMT2.thy	Thu Jun 12 17:10:12 2014 +0200
     3.2 +++ b/src/HOL/SMT2.thy	Thu Jun 12 17:50:49 2014 +0200
     3.3 @@ -200,6 +200,7 @@
     3.4  *}
     3.5  
     3.6  declare [[cvc3_new_options = ""]]
     3.7 +declare [[cvc4_new_options = ""]]
     3.8  declare [[z3_new_options = ""]]
     3.9  
    3.10  text {*