| 12345678910111213141516171819202122232425262728293031323334 |
- --- Isabelle2016-1-orig/src/HOL/SMT_Examples/Boogie.thy 2016-12-13 01:03:38.000000000 +1100
- +++ Isabelle2016-1/src/HOL/SMT_Examples/Boogie.thy 2016-12-30 23:46:11.947737290 +1100
- @@ -52,7 +52,7 @@
- section \<open>Verification condition proofs\<close>
-
- declare [[smt_oracle = false]]
- -declare [[smt_read_only_certificates = true]]
- +declare [[smt_read_only_certificates = false]]
-
-
- declare [[smt_certificates = "Boogie_Max.certs"]]
- --- Isabelle2016-1-orig/src/HOL/SMT_Examples/SMT_Examples.thy 2016-12-13 01:03:38.000000000 +1100
- +++ Isabelle2016-1/src/HOL/SMT_Examples/SMT_Examples.thy 2016-12-30 23:46:11.953737338 +1100
- @@ -9,7 +9,7 @@
- begin
-
- declare [[smt_certificates = "SMT_Examples.certs"]]
- -declare [[smt_read_only_certificates = true]]
- +declare [[smt_read_only_certificates = false]]
-
-
- section \<open>Propositional and first-order logic\<close>
- --- Isabelle2016-1-orig/src/HOL/SMT_Examples/SMT_Word_Examples.thy 2016-12-13 01:03:38.000000000 +1100
- +++ Isabelle2016-1/src/HOL/SMT_Examples/SMT_Word_Examples.thy 2016-12-30 23:46:11.967737450 +1100
- @@ -11,7 +11,7 @@
- declare [[smt_oracle = true]]
- declare [[z3_extensions = true]]
- declare [[smt_certificates = "SMT_Word_Examples.certs"]]
- -declare [[smt_read_only_certificates = true]]
- +declare [[smt_read_only_certificates = false]]
-
- text \<open>
- Currently, there is no proof reconstruction for words.
|
