Mercurial
Mercurial
>
repos
>
isabelle
/ file revisions
summary
|
shortlog
|
changelog
|
graph
|
tags
|
bookmarks
|
branches
|
file
| revisions |
annotate
|
diff
|
comparison
|
rss
|
help
(0)
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
src/HOL/Tools/SMT/z3_model.ML
Tue, 30 Nov 2010 18:22:43 +0100
boehmes
split up Z3 models into constraints on free variables and constant definitions;
file
|
diff
|
annotate
Mon, 22 Nov 2010 15:45:43 +0100
boehmes
share and use more utility functions;
file
|
diff
|
annotate
Sat, 20 Nov 2010 00:53:26 +0100
wenzelm
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
file
|
diff
|
annotate
Wed, 17 Nov 2010 08:14:56 +0100
boehmes
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
file
|
diff
|
annotate
Mon, 15 Nov 2010 17:52:48 +0100
boehmes
only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers
file
|
diff
|
annotate
Sun, 19 Sep 2010 11:33:39 +0200
boehmes
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
file
|
diff
|
annotate
Thu, 27 May 2010 16:29:33 +0200
boehmes
renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")
file
|
diff
|
annotate
Wed, 12 May 2010 23:54:02 +0200
boehmes
integrated SMT into the HOL image
file
|
diff
|
annotate
less
more
(0)
tip