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
.
restricted Z3 by default to a fragment where proof reconstruction should not fail (for better integration with Sledgehammer) -- the full set of supported Z3 features can still be used by enabling the configuration option "z3_with_extensions"
author
boehmes
Mon, 04 Jun 2012 09:07:23 +0200
changeset 48069
e9b2782c4f99
parent 48068
04aeda922be2
child 48071
d7864276bca8
restricted Z3 by default to a fragment where proof reconstruction should not fail (for better integration with Sledgehammer) -- the full set of supported Z3 features can still be used by enabling the configuration option "z3_with_extensions"
NEWS
file
|
annotate
|
diff
|
comparison
|
revisions
src/HOL/Boogie/Examples/VCC_Max.thy
file
|
annotate
|
diff
|
comparison
|
revisions
src/HOL/Multivariate_Analysis/Integration.thy
file
|
annotate
|
diff
|
comparison
|
revisions
src/HOL/SMT_Examples/SMT_Examples.thy
file
|
annotate
|
diff
|
comparison
|
revisions
src/HOL/SMT_Examples/SMT_Tests.thy
file
|
annotate
|
diff
|
comparison
|
revisions
src/HOL/Tools/SMT/smt_setup_solvers.ML
file
|
annotate
|
diff
|