[isabelle-dev] smt2

[Jasmin Blanchette]

Hi Larry,

Am 15.03.2014 um 16:27 schrieb Lawrence Paulson <lp15 at cam.ac.uk>:

> But working very well, in my experience.

I'm glad to hear that. :)

> Now, will smt2 calls be suitable for the Library and AFP?

No, because they suffer from the exact same issues as "smt" calls. We could of course rethink our policy, but this is orthogonal to "smt" vs. "smt2".

Instead, I put all my hopes in the Isar proof construction. There are myriads of little engineering details to solve (e.g., mimicking in Isar some of the preprocessing that "smt2" does, e.g., embedding "nat"s into "int"s), but I am confident we should have something rather solid in place within a couple of months.

Jasmin