But working very well, in my experience. Now, will smt2 calls be suitable for the Library and AFP?
Larry On 6 Mar 2014, at 15:43, Jasmin Christian Blanchette <jasmin.blanche...@gmail.com> wrote: > As you may know, Sascha and I have been working on a new version of the "smt" > proof method, called "smt2". It is effectively a clone of "smt", but with the > Z3 interaction (problem generation, proof parsing, and reconstruction) > rewritten from scratch, with the following short-term goals: > > 1. Use SMT-LIB 2 instead of 1. > 2. Support newer versions of Z3 (> 4.0). > 3. Produce Isar proofs from Z3 proofs. > > It is still highly experimental _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
