src/HOL/Multivariate_Analysis/Integration.thy
changeset 35945 fcd02244e63d
parent 35752 c8a8df426666
child 36081 70deefb6c093
     1.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Wed Mar 24 12:30:21 2010 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Wed Mar 24 14:03:52 2010 +0100
     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_record=true]]
     1.8 +declare [[smt_record=false]]
     1.9  declare [[z3_proofs=true]]
    1.10  
    1.11  lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto