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

[Sascha Boehme]

Hi,

Zitat von Ond?ej Kun?ar <kuncar at in.tum.de>:
>
> 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.

I do have an idea what might go wrong. I'll need to investigate it  
further before committing a patch.

Cheers,
Sascha