[isabelle-dev] E 1.3 is out

[Jasmin Blanchette]

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