blob: d766a957021d6394bb0f9314325da5a7930a1c73 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
--- 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.
|
GitWeb
