History log of /seL4-l4v-10.1.1/HOL4/src/HolSmt/Z3_Proof.sml
Revision Date Author Comments
# 66540042 04-Sep-2011 Tjark Weber <tw333@cl.cam.ac.uk>

Added support for Z3's proof rule IFF_TRUE.
# b3643b11 25-Oct-2010 Tjark Weber <Tjark.Weber@cl.cam.ac.uk>

Z3 proof parser updated for Z3 2.13. The proof parser now uses the SMT-LIB
benchmark parser internally.
# 8f132552 20-Sep-2010 Tjark Weber <Tjark.Weber@cl.cam.ac.uk>

Major update, adding support for Z3 2.11 proofs (SMT-LIB 2 format).

Note that this breaks Z3 proof checking from HOL4 (for now), as no translation
from HOL4 into SMT-LIB 2 has been implemented yet.
# 8cf47a52 29-Sep-2009 Tjark Weber <Tjark.Weber@cl.cam.ac.uk>

HolSmtLib now supports the Z3 2.0 proof format.