On 11/08/2012 11:59 AM, Tobias Nipkow wrote:
This is exactly why I am against SMT certificates in AFP entries. Ondrej, can
you possibly remove them?
All SMT calls are now removed (changeset 3685878ce7b7).
But AVL-Trees were already broken in Isabelle's changeset 791157a4179a
(ensured that rewr_conv rule t = "t == u" literally not just modulo
beta-eta) before Jasmin's changeset 34b0464d7eef. It seems that the
changeset fixing rewr_conv interacts with smt. There is a goal which is
the same goal before and after the change - the term is really the same;
no tricks like the pretty-printer does beta-reduction.
And smt fails only after the change and it doesn't matter if the
pregenerated certificates are used. Somebody who understands smt should
take a look at how much the changeset with rewr_conv is harmful to smt.
Ondrej
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
