isabelle: File revisions

src/HOL/SMT/Tools/cvc3_solver.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)	file \| diff \| annotate
Fri, 13 Nov 2009 15:47:37 +0100	boehmes	removed unused code and unused arguments,	file \| diff \| annotate
Fri, 06 Nov 2009 17:52:57 +0100	boehmes	added documentation for local SMT solver setup and available SMT options,	file \| diff \| annotate
Tue, 03 Nov 2009 14:51:55 +0100	boehmes	added a specific SMT exception captured by smt_tac (prevents the SMT method from failing with an exception),	file \| diff \| annotate
Fri, 30 Oct 2009 11:27:47 +0100	boehmes	disable printing of unparsed counterexamples for CVC3 and Yices	file \| diff \| annotate
Tue, 20 Oct 2009 14:22:02 +0200	boehmes	eliminated extraneous wrapping of public records,	file \| diff \| annotate
Tue, 20 Oct 2009 10:11:30 +0200	boehmes	added proof reconstructon for Z3,	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

isabelle