# HG changeset patch # User blanchet # Date 1506909535 -7200 # Node ID c90fb8bee1dd2f24fb4c93060a1f99be17a3199f # Parent ece9435ca78e45ea25f9de430505283509095229 repaired small incident diff -r ece9435ca78e -r c90fb8bee1dd src/HOL/SMT_Examples/Boogie.thy --- 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 \Verification condition proofs\ declare [[smt_oracle = false]] -declare [[smt_read_only_certificates = false]] (* FIXME *) +declare [[smt_read_only_certificates = true]] declare [[smt_certificates = "Boogie_Max.certs"]]