src/HOL/Multivariate_Analysis/Integration.thy

     show "\<exists>B>0. \<forall>a b. ball 0 B \<subseteq> {a..b} \<longrightarrow>
                     norm (integral {a..b} (\<lambda>x. if x \<in> s then f x else 0) - i) < e"
     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