[isabelle-dev] Status of HOL/SMT

[Makarius]

On Tue, 4 Dec 2012, Jasmin Blanchette wrote:

> In general, we should try to reduce our exposure to SMT proofs in 
> Isabelle (and keep it to 0 in the AFP). That "SMT_Examples" use them is 
> fine, but any "smt" call that can be replaced by something else in other 
> places, e.g. "Multivariate_Analysis", should be done in the long term. 
> It's something where the Sledgehammer Isar proof generation framework 
> should help at some point (e.g. in one year from now) -- once we're done 
> with the ATP side we'll see what can be done with SMT proofs.

Multivariate_Analysis is a bit odd in many ways, not just spurious use of 
smt.  I usually see this as an opportunity for gradual clean-up, providing 
good tools for that, which can be used in other situations as well.

For you it is better Sledgehammer/SMT support to inline better proof 
steps.

For me it is something like plain-old auto-indentation and reformatting in 
Isabelle/jEdit to get the theory sources into a sane state, where they can 
be read and edited normally.  Some weeks ago I've already fine-tuned my 
buffer overview column to make it work smoothly with these unusually large 
files.


 	Makarius