src/HOL/Tools/SMT/smt_real.ML
Wed, 08 Dec 2010 08:33:02 +0100 boehmes be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
Tue, 07 Dec 2010 14:53:12 +0100 boehmes centralized handling of built-in types and constants;
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)
Fri, 12 Nov 2010 15:56:11 +0100 boehmes preliminary support for newer versions of Z3
Wed, 25 Aug 2010 18:36:22 +0200 wenzelm renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
Wed, 12 May 2010 23:54:04 +0200 boehmes layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
less more (0) tip