Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
inhibit invokation of external SMT solver
authorboehmes
Wed, 24 Mar 2010 14:03:52 +0100
changeset 35945 fcd02244e63d
parent 35944 c53a6865111b
child 35946 7a86d7706106
inhibit invokation of external SMT solver
src/HOL/Multivariate_Analysis/Integration.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Wed Mar 24 12:30:21 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Wed Mar 24 14:03:52 2010 +0100
@@ -8,7 +8,7 @@
 begin
 
 declare [[smt_certificates="~~/src/HOL/Multivariate_Analysis/Integration.cert"]]
-declare [[smt_record=true]]
+declare [[smt_record=false]]
 declare [[z3_proofs=true]]
 
 lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto
isabelle