merged
authorwenzelm
Mon, 02 Oct 2017 16:47:46 +0200
changeset 66754 78c74f9e960a
parent 66741 c90fb8bee1dd (diff)
parent 66753 f7759beab4f2 (current diff)
child 66755 1ceedf710564
merged
--- a/src/HOL/SMT_Examples/Boogie.thy	Mon Oct 02 16:42:12 2017 +0200
+++ b/src/HOL/SMT_Examples/Boogie.thy	Mon Oct 02 16:47:46 2017 +0200
@@ -52,7 +52,7 @@
 section \<open>Verification condition proofs\<close>
 
 declare [[smt_oracle = false]]
-declare [[smt_read_only_certificates = false]] (* FIXME *)
+declare [[smt_read_only_certificates = true]]
 
 
 declare [[smt_certificates = "Boogie_Max.certs"]]