[isabelle] ismt update

We are pleased to announce that ismt, our external oracle to SRI's Yices SMT solver, is now compatible with Isabelle2009-2 and Yices v1.0.28.


The main novelty of ismt is that it communicates with Yices in Yices' native formula language, which is richer than SMT-LIB. For example, Isabelle datatypes are translated directly into Yices datatypes.


- Levent Erkok and John Matthews

Attachment: smime.p7s
Description: S/MIME cryptographic signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.