| Sun, 28 Mar 2010 16:59:06 +0200 |
wenzelm |
static defaults for configuration options;
|
file |
diff |
annotate
|
| Thu, 11 Feb 2010 17:48:55 +0100 |
boehmes |
unfold quantifiers (Ball, Bex, Ex1)
|
file |
diff |
annotate
|
| Thu, 03 Dec 2009 15:56:06 +0100 |
boehmes |
faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
|
file |
diff |
annotate
|
| Wed, 25 Nov 2009 12:30:54 +0100 |
boehmes |
only add nat/int conversion rules if necessary
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 15:47:37 +0100 |
boehmes |
removed unused code and unused arguments,
|
file |
diff |
annotate
|
| Fri, 30 Oct 2009 11:31:34 +0100 |
boehmes |
abstract over variables in reversed order (application uses given order)
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 10:52:05 +0100 |
boehmes |
simplified method syntax of "smt",
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 17:34:00 +0100 |
wenzelm |
normalized basic type abbreviations;
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 10:11:30 +0200 |
boehmes |
added proof reconstructon for Z3,
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 16:24:36 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Fri, 18 Sep 2009 18:13:19 +0200 |
boehmes |
added new method "smt": an oracle-based connection to external SMT solvers
|
file |
diff |
annotate
|