2010-11-22 boehmes 2010-11-22 share and use more utility functions; slightly reduced complexity for Z3 proof rule 'rewrite'
2010-11-20 wenzelm 2010-11-20 renamed raw "explode" function to "raw_explode" to emphasize its meaning;
2010-11-17 boehmes 2010-11-17 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)
2010-11-15 boehmes 2010-11-15 only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers
2010-09-19 boehmes 2010-09-19 properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
2010-05-27 boehmes 2010-05-27 renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")
2010-05-12 boehmes 2010-05-12 integrated SMT into the HOL image