--- a/src/HOL/Multivariate_Analysis/Integration.thy Sun Jan 16 21:10:30 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Mon Jan 17 17:45:52 2011 +0100
@@ -12,7 +12,7 @@
declare [[smt_certificates="Integration.certs"]]
declare [[smt_fixed=true]]
-declare [[smt_solver=z3, smt_oracle=false]]
+declare [[smt_oracle=false]]
setup {* Arith_Data.add_tactic "Ferrante-Rackoff" (K FerranteRackoff.dlo_tac) *}
@@ -5527,6 +5527,5 @@
declare [[smt_certificates=""]]
declare [[smt_fixed=false]]
-declare [[smt_solver=cvc3]]
end