| changeset 40513 | 1204d268464f |
| parent 40163 | a462d5207aa6 |
| child 41413 | 64cd30d6b0b8 |
--- a/src/HOL/Multivariate_Analysis/Integration.thy Fri Nov 12 15:56:06 2010 +0100 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Fri Nov 12 15:56:07 2010 +0100 @@ -7,7 +7,7 @@ imports Derivative "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Indicator_Function begin -declare [[smt_certificates="~~/src/HOL/Multivariate_Analysis/Integration.certs"]] +declare [[smt_certificates="Integration.certs"]] declare [[smt_fixed=true]] declare [[smt_oracle=false]]