src/HOL/SMT_Examples/Boogie.thy
changeset 66741 c90fb8bee1dd
parent 66740 ece9435ca78e
child 66758 9312ce5a938d
     1.1 --- a/src/HOL/SMT_Examples/Boogie.thy	Sun Oct 01 15:17:43 2017 +0200
     1.2 +++ b/src/HOL/SMT_Examples/Boogie.thy	Mon Oct 02 03:58:55 2017 +0200
     1.3 @@ -52,7 +52,7 @@
     1.4  section \<open>Verification condition proofs\<close>
     1.5  
     1.6  declare [[smt_oracle = false]]
     1.7 -declare [[smt_read_only_certificates = false]] (* FIXME *)
     1.8 +declare [[smt_read_only_certificates = true]]
     1.9  
    1.10  
    1.11  declare [[smt_certificates = "Boogie_Max.certs"]]