[isabelle] How to invoke Z3 from Isabelle

Dear all!

I am currently learning how to use Z3 SMT solver. I program in Java, unfortunately, Z3 does not interface with Java.
Luckily , I read about Isabelle but I don't have an idea on how to use it, nor how to invoke Z3 from Isabelle.

Please I will appreciate any help offered to me in this regard, especially if there is a link I can download detailed and self explanatory tutorial on how to Invoke Z3 from Isabelle.


Joshua  Nwokeji
School of Engineering and Information Sciences (EIS),
Middlesex University, London

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