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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
