Only use provided SMT-certificates in HOL-Multivariate_Analysis.
--- a/src/HOL/Multivariate_Analysis/Integration.thy Tue Apr 20 14:07:52 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Wed Apr 21 10:44:44 2010 +0200
@@ -8,7 +8,7 @@
begin
declare [[smt_certificates="~~/src/HOL/Multivariate_Analysis/Integration.cert"]]
-declare [[smt_fixed=false]]
+declare [[smt_fixed=true]]
declare [[z3_proofs=true]]
subsection {* Sundries *}
@@ -5525,5 +5525,6 @@
qed qed(insert n,auto) qed qed qed
declare [[smt_certificates=""]]
+declare [[smt_fixed=false]]
end