--- a/src/HOL/SMT_Examples/Boogie.thy Thu Aug 28 00:40:38 2014 +0200
+++ b/src/HOL/SMT_Examples/Boogie.thy Thu Aug 28 00:40:38 2014 +0200
@@ -51,22 +51,22 @@
section {* Verification condition proofs *}
-declare [[smt2_oracle = false]]
-declare [[smt2_read_only_certificates = true]]
+declare [[smt_oracle = false]]
+declare [[smt_read_only_certificates = true]]
-declare [[smt2_certificates = "Boogie_Max.certs2"]]
+declare [[smt_certificates = "Boogie_Max.certs2"]]
boogie_file Boogie_Max
-declare [[smt2_certificates = "Boogie_Dijkstra.certs2"]]
+declare [[smt_certificates = "Boogie_Dijkstra.certs2"]]
boogie_file Boogie_Dijkstra
-declare [[z3_new_extensions = true]]
-declare [[smt2_certificates = "VCC_Max.certs2"]]
+declare [[z3_extensions = true]]
+declare [[smt_certificates = "VCC_Max.certs2"]]
boogie_file VCC_Max