| Tue, 26 Oct 2010 11:45:12 +0200 |
boehmes |
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 11:39:26 +0200 |
boehmes |
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
|
file |
diff |
annotate
|
| Fri, 01 Oct 2010 10:25:36 +0200 |
haftmann |
chop_while replace drop_while and take_while
|
file |
diff |
annotate
|
| Thu, 30 Sep 2010 18:37:29 +0200 |
haftmann |
take_while, drop_while
|
file |
diff |
annotate
|
| Fri, 17 Sep 2010 10:52:35 +0200 |
boehmes |
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 17:59:40 +0200 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Mon, 17 May 2010 23:54:15 +0200 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file |
diff |
annotate
|
| Sat, 15 May 2010 16:20:54 +0200 |
blanchet |
make SML/NJ happy
|
file |
diff |
annotate
|
| Wed, 12 May 2010 23:54:04 +0200 |
boehmes |
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
|
file |
diff |
annotate
|
| Wed, 12 May 2010 23:54:02 +0200 |
boehmes |
integrated SMT into the HOL image
|
file |
diff |
annotate
|