| Wed, 12 May 2010 23:54:00 +0200 | use proper context operations (for fresh names of type and term variables, and for hypothetical definitions), monomorphize theorems (instead of terms, necessary for hypothetical definitions made during lambda lifting) | file | diff | annotate |
| Thu, 03 Dec 2009 15:56:06 +0100 | 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, 21 Oct 2009 12:19:46 +0200 | proper handling of single literal case, | file | diff | annotate |
| Wed, 21 Oct 2009 08:14:38 +0200 | dropped redundant gen_ prefix | file | diff | annotate |
| Thu, 15 Oct 2009 21:28:39 +0200 | normalized aliases of Output operations; | file | diff | annotate |
| Fri, 18 Sep 2009 18:13:19 +0200 | added new method "smt": an oracle-based connection to external SMT solvers | file | diff | annotate |