| changeset 40163 | a462d5207aa6 |
| parent 39302 | d7728f65b353 |
| child 40513 | 1204d268464f |
--- a/src/HOL/Multivariate_Analysis/Integration.thy Tue Oct 26 11:45:12 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Tue Oct 26 11:46:19 2010 +0200 @@ -8,8 +8,8 @@ begin declare [[smt_certificates="~~/src/HOL/Multivariate_Analysis/Integration.certs"]] -declare [[smt_fixed=false]] -declare [[z3_proofs=true]] +declare [[smt_fixed=true]] +declare [[smt_oracle=false]] setup {* Arith_Data.add_tactic "Ferrante-Rackoff" (K FerranteRackoff.dlo_tac) *}