src/HOL/SMT/SMT_Base.thy
Wed, 12 May 2010 23:53:48 +0200 boehmes moved the addition of DLO tactic into the Z3 theory (DLO is required only for Z3 proof reconstruction)
Wed, 07 Apr 2010 20:40:42 +0200 boehmes always unfold definitions of specific constants (including special binders)
Wed, 24 Mar 2010 09:44:47 +0100 boehmes cache_io is now just a single ML file instead of a component
Tue, 16 Feb 2010 15:25:36 +0100 boehmes added Cache_IO: cache for output of external tools,
Thu, 11 Feb 2010 09:14:08 +0100 boehmes use full paths when importing theories
Fri, 22 Jan 2010 16:38:21 +0100 boehmes support skolem constant for extensional arrays in Z3 proofs
Tue, 27 Oct 2009 18:09:11 +0100 boehmes removed unused file smt_builtin.ML,
Tue, 20 Oct 2009 10:11:30 +0200 boehmes added proof reconstructon for Z3,
less more (0) tip