src/HOL/SMT_Examples/Boogie.thy
changeset 58061 3d060f43accb
parent 56818 689a3eeb6f9e
child 58367 8af1e68d7e1a
     1.1 --- a/src/HOL/SMT_Examples/Boogie.thy	Thu Aug 28 00:40:38 2014 +0200
     1.2 +++ b/src/HOL/SMT_Examples/Boogie.thy	Thu Aug 28 00:40:38 2014 +0200
     1.3 @@ -51,22 +51,22 @@
     1.4  
     1.5  section {* Verification condition proofs *}
     1.6  
     1.7 -declare [[smt2_oracle = false]]
     1.8 -declare [[smt2_read_only_certificates = true]]
     1.9 +declare [[smt_oracle = false]]
    1.10 +declare [[smt_read_only_certificates = true]]
    1.11  
    1.12  
    1.13 -declare [[smt2_certificates = "Boogie_Max.certs2"]]
    1.14 +declare [[smt_certificates = "Boogie_Max.certs2"]]
    1.15  
    1.16  boogie_file Boogie_Max
    1.17  
    1.18  
    1.19 -declare [[smt2_certificates = "Boogie_Dijkstra.certs2"]]
    1.20 +declare [[smt_certificates = "Boogie_Dijkstra.certs2"]]
    1.21  
    1.22  boogie_file Boogie_Dijkstra
    1.23  
    1.24  
    1.25 -declare [[z3_new_extensions = true]]
    1.26 -declare [[smt2_certificates = "VCC_Max.certs2"]]
    1.27 +declare [[z3_extensions = true]]
    1.28 +declare [[smt_certificates = "VCC_Max.certs2"]]
    1.29  
    1.30  boogie_file VCC_Max
    1.31