[isabelle-dev] AFP: Session AVL-Trees broken
kuncar at in.tum.de
Fri Nov 9 19:12:13 CET 2012
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.
More information about the isabelle-dev