--- 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