# HG changeset patch
# User himmelma
# Date 1268145743 -3600
# Node ID c8a8df426666c10fa7ecc156f3a1c4017807e912
# Parent  f7f8d59b60b9d80a181e22be6177e84c86b56e97
reset smt_certificates

diff -r f7f8d59b60b9 -r c8a8df426666 src/HOL/Multivariate_Analysis/Integration.thy
--- 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