# HG changeset patch
# User hoelzl
# Date 1271839484 -7200
# Node ID 009b0ee1b8386534846c5978a1dea11969b5a6c3
# Parent  027ae62681be53412ab9ea79207b34200ebb30d1
Only use provided SMT-certificates in HOL-Multivariate_Analysis.

diff -r 027ae62681be -r 009b0ee1b838 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Apr 20 14:07:52 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Wed Apr 21 10:44:44 2010 +0200
@@ -8,7 +8,7 @@
 begin
 
 declare [[smt_certificates="~~/src/HOL/Multivariate_Analysis/Integration.cert"]]
-declare [[smt_fixed=false]]
+declare [[smt_fixed=true]]
 declare [[z3_proofs=true]]
 
 subsection {* Sundries *}
@@ -5525,5 +5525,6 @@
         qed qed(insert n,auto) qed qed qed
 
 declare [[smt_certificates=""]]
+declare [[smt_fixed=false]]
 
 end