src/HOL/Tools/SMT/z3_proof_reconstruction.ML
Wed, 01 Sep 2010 15:33:59 +0200 haftmann replaced Table.map' by Table.map
Fri, 27 Aug 2010 10:56:46 +0200 haftmann formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
Wed, 26 May 2010 17:52:32 +0200 boehmes try logical and theory abstraction before full abstraction (avoids warnings of linarith)
Sat, 15 May 2010 17:59:06 +0200 wenzelm incorporated further conversions and conversionals, after some minor tuning;
Wed, 12 May 2010 23:54:04 +0200 boehmes layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
Wed, 12 May 2010 23:54:02 +0200 boehmes integrated SMT into the HOL image
less more (0) tip