src/HOL/Boogie/Examples/Boogie_Max.thy
changeset 33445 f0c78a28e18e
parent 33424 a3b002e2cd55
child 33663 a84fd6385832
     1.1 --- a/src/HOL/Boogie/Examples/Boogie_Max.thy	Thu Nov 05 14:41:37 2009 +0100
     1.2 +++ b/src/HOL/Boogie/Examples/Boogie_Max.thy	Thu Nov 05 14:48:40 2009 +0100
     1.3 @@ -41,9 +41,9 @@
     1.4  text {*
     1.5  Approach 1: Discharge the verification condition fully automatically by SMT:
     1.6  *}
     1.7 -boogie_vc b_max
     1.8 +boogie_vc max
     1.9    unfolding labels
    1.10 -  using [[smt_cert="~~/src/HOL/Boogie/Examples/cert/Boogie_b_max"]]
    1.11 +  using [[smt_cert="~~/src/HOL/Boogie/Examples/cert/Boogie_max"]]
    1.12    using [[z3_proofs=true]]
    1.13    by (smt boogie)
    1.14  
    1.15 @@ -53,7 +53,7 @@
    1.16  explicit proof. This approach is most useful in an interactive debug-and-fix
    1.17  mode. 
    1.18  *}
    1.19 -boogie_vc b_max
    1.20 +boogie_vc max
    1.21  proof (split_vc (verbose) try: fast simp)
    1.22    print_cases
    1.23    case L_14_5c