src/HOL/SMT/Tools/smt_monomorph.ML
Wed, 12 May 2010 23:54:00 +0200 boehmes 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)
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),
Wed, 21 Oct 2009 12:19:46 +0200 boehmes proper handling of single literal case,
Wed, 21 Oct 2009 08:14:38 +0200 haftmann dropped redundant gen_ prefix
Thu, 15 Oct 2009 21:28:39 +0200 wenzelm normalized aliases of Output operations;
Fri, 18 Sep 2009 18:13:19 +0200 boehmes added new method "smt": an oracle-based connection to external SMT solvers
less more (0) tip