src/HOL/Tools/SMT/z3_model.ML
Mon, 06 Dec 2010 16:54:22 +0100 boehmes more aggressive unfolding of unknowns in Z3 models
Wed, 01 Dec 2010 13:09:08 +0100 wenzelm just one Term.dest_funT;
Tue, 30 Nov 2010 18:22:43 +0100 boehmes split up Z3 models into constraints on free variables and constant definitions;
Mon, 22 Nov 2010 15:45:43 +0100 boehmes share and use more utility functions;
Sat, 20 Nov 2010 00:53:26 +0100 wenzelm renamed raw "explode" function to "raw_explode" to emphasize its meaning;
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)
Mon, 15 Nov 2010 17:52:48 +0100 boehmes only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers
Sun, 19 Sep 2010 11:33:39 +0200 boehmes properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
Thu, 27 May 2010 16:29:33 +0200 boehmes renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")
Wed, 12 May 2010 23:54:02 +0200 boehmes integrated SMT into the HOL image
less more (0) tip