
diff -r 138f414f14cb -r 3214c39777ab src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Jan 04 15:46:38 2011 -0800
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Thu Jan 06 17:51:56 2011 +0100
@@ -12,7 +12,7 @@
 
 declare [[smt_certificates="Integration.certs"]]
 declare [[smt_fixed=true]]
-declare [[smt_oracle=false]]
+declare [[smt_solver=z3, smt_oracle=false]]
 
 setup {* Arith_Data.add_tactic "Ferrante-Rackoff" (K FerranteRackoff.dlo_tac) *}
 
@@ -5527,5 +5527,6 @@
 
 declare [[smt_certificates=""]]
 declare [[smt_fixed=false]]
+declare [[smt_solver=cvc3]]
 
 end




