# HG changeset patch
# User boehmes
# Date 1269435832 -3600
# Node ID fcd02244e63d018b8584635cf5957dc511dd1719
# Parent  c53a6865111bc7b9f627a42a3add6157dcc558e2
inhibit invokation of external SMT solver

diff -r c53a6865111b -r fcd02244e63d src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Wed Mar 24 12:30:21 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Wed Mar 24 14:03:52 2010 +0100
@@ -8,7 +8,7 @@
 begin
 
 declare [[smt_certificates="~~/src/HOL/Multivariate_Analysis/Integration.cert"]]
-declare [[smt_record=true]]
+declare [[smt_record=false]]
 declare [[z3_proofs=true]]
 
 lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto