src/HOL/Boogie/Examples/Boogie_Dijkstra.thy

--- a/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy	Tue Oct 26 11:45:12 2010 +0200
+++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy	Tue Oct 26 11:46:19 2010 +0200
@@ -83,9 +83,9 @@
 
 declare [[smt_certificates="~~/src/HOL/Boogie/Examples/Boogie_Dijkstra.certs"]]
 declare [[smt_fixed=true]]
+declare [[smt_oracle=false]]
 
 boogie_vc Dijkstra
-  using [[z3_proofs=true]]
   by boogie
 
 boogie_end