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