src/HOL/Boogie/Examples/Boogie_Dijkstra.thy
changeset 40513 1204d268464f
parent 40163 a462d5207aa6
child 40514 db5f14910dce
equal deleted inserted replaced
40512:fd218201da5e 40513:1204d268464f
    79 *}
    79 *}
    80 
    80 
    81 
    81 
    82 boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Dijkstra"
    82 boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Dijkstra"
    83 
    83 
    84 declare [[smt_certificates="~~/src/HOL/Boogie/Examples/Boogie_Dijkstra.certs"]]
    84 declare [[smt_certificates="Boogie_Dijkstra.certs"]]
    85 declare [[smt_fixed=true]]
    85 declare [[smt_fixed=true]]
    86 declare [[smt_oracle=false]]
    86 declare [[smt_oracle=false]]
    87 
    87 
    88 boogie_vc Dijkstra
    88 boogie_vc Dijkstra
    89   by boogie
    89   by boogie