| changeset 40514 | db5f14910dce |
| parent 40513 | 1204d268464f |
| child 40540 | 293f9f211be0 |
--- a/src/HOL/Boogie/Examples/Boogie_Max.thy Fri Nov 12 15:56:07 2010 +0100 +++ b/src/HOL/Boogie/Examples/Boogie_Max.thy Fri Nov 12 15:56:08 2010 +0100 @@ -36,7 +36,7 @@ \end{verbatim} *} -boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Max" +boogie_open "Boogie_Max" declare [[smt_certificates="Boogie_Max.certs"]] declare [[smt_fixed=true]]