[isabelle-dev] AFP: Session AVL-Trees broken

[Ondřej Kunčar]

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