author | blanchet |
Mon, 02 Oct 2017 03:58:55 +0200 | |
changeset 66741 | c90fb8bee1dd |
parent 66740 | ece9435ca78e |
child 66754 | 78c74f9e960a |
--- a/src/HOL/SMT_Examples/Boogie.thy Sun Oct 01 15:17:43 2017 +0200 +++ b/src/HOL/SMT_Examples/Boogie.thy Mon Oct 02 03:58:55 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"]]