src/HOL/Multivariate_Analysis/Integration.thy
changeset 35752 c8a8df426666
parent 35751 f7f8d59b60b9
child 35945 fcd02244e63d
     1.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Mar 09 15:39:26 2010 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Mar 09 15:42:23 2010 +0100
     1.3 @@ -3908,4 +3908,8 @@
     1.4      proof(rule,rule,rule B,safe) case goal1 from B(2)[OF this] guess z .. note z=conjunctD2[OF this]
     1.5        from integral_unique[OF this(1)] show ?case using z(2) by auto qed qed qed 
     1.6  
     1.7 +
     1.8 +
     1.9 +declare [[smt_certificates=""]]
    1.10 +
    1.11  end