author | wenzelm |
Mon, 02 Oct 2017 16:47:46 +0200 | |
changeset 66754 | 78c74f9e960a |
parent 66741 | c90fb8bee1dd (diff) |
parent 66753 | f7759beab4f2 (current diff) |
child 66755 | 1ceedf710564 |
--- 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"]]