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