changeset 36081 | 70deefb6c093 |
parent 35945 | fcd02244e63d |
child 36243 | 027ae62681be |
--- a/src/HOL/Multivariate_Analysis/Integration.thy Wed Apr 07 17:24:44 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Wed Apr 07 19:48:58 2010 +0200 @@ -8,7 +8,7 @@ begin declare [[smt_certificates="~~/src/HOL/Multivariate_Analysis/Integration.cert"]] -declare [[smt_record=false]] +declare [[smt_fixed=true]] declare [[z3_proofs=true]] lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto