reset smt_certificates

--- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Mar 09 15:39:26 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Mar 09 15:42:23 2010 +0100
@@ -3908,4 +3908,8 @@
     proof(rule,rule,rule B,safe) case goal1 from B(2)[OF this] guess z .. note z=conjunctD2[OF this]
       from integral_unique[OF this(1)] show ?case using z(2) by auto qed qed qed 
 
+
+
+declare [[smt_certificates=""]]
+
 end