Hi all, E 1.3 was secretly released on Sunday, and with it an extremely cool feature: "Weight functions that allow the user to focus the search on certain function symbols" [1]. This feature was motivated by Sledgehammer and is used for all its worth so that those lemmas that seem more relevant a priori are given more weight. It makes a significant difference in practice (enough that E now beats Vampire), so if you are a heavy Sledgehammer user you might want to download and untar the package [2], and make sure to update "~/.isabelle/etc/components" with the new path (or "~/.isabelle/etc/settings" if you use the "init_component" idiom).
[1] http://www4.informatik.tu-muenchen.de/~schulz/E/E.html [2] http://www4.in.tum.de/~blanchet/e-1.3.tgz Jasmin _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
