Hi, Zitat von Ond?ej Kun?ar <[email protected]>:
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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
