inhibit invokation of external SMT solver
authorboehmes
Wed Mar 24 14:03:52 2010 +0100 (2010-03-24)
changeset 35945fcd02244e63d
parent 35944 c53a6865111b
child 35946 7a86d7706106
inhibit invokation of external SMT solver
src/HOL/Multivariate_Analysis/Integration.thy
     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