Only use provided SMT-certificates in HOL-Multivariate_Analysis.
authorhoelzl
Wed Apr 21 10:44:44 2010 +0200 (2010-04-21)
changeset 36244009b0ee1b838
parent 36243 027ae62681be
child 36245 af5fe3a72087
Only use provided SMT-certificates in HOL-Multivariate_Analysis.
src/HOL/Multivariate_Analysis/Integration.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Apr 20 14:07:52 2010 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Wed Apr 21 10:44:44 2010 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  begin
     1.5  
     1.6  declare [[smt_certificates="~~/src/HOL/Multivariate_Analysis/Integration.cert"]]
     1.7 -declare [[smt_fixed=false]]
     1.8 +declare [[smt_fixed=true]]
     1.9  declare [[z3_proofs=true]]
    1.10  
    1.11  subsection {* Sundries *}
    1.12 @@ -5525,5 +5525,6 @@
    1.13          qed qed(insert n,auto) qed qed qed
    1.14  
    1.15  declare [[smt_certificates=""]]
    1.16 +declare [[smt_fixed=false]]
    1.17  
    1.18  end