| changeset 34068 | a78307d72e58 |
| parent 33445 | f0c78a28e18e |
| child 34993 | bf3b8462732b |
--- a/src/HOL/Boogie/Examples/VCC_Max.thy Fri Dec 11 15:06:12 2009 +0100 +++ b/src/HOL/Boogie/Examples/VCC_Max.thy Fri Dec 11 15:35:29 2009 +0100 @@ -49,10 +49,9 @@ boogie_status boogie_vc maximum - unfolding labels + using [[z3_proofs=true]] using [[smt_cert="~~/src/HOL/Boogie/Examples/cert/VCC_maximum"]] - using [[z3_proofs=true]] - by (smt boogie) + by boogie boogie_end