[isabelle-dev] E 1.3 is out
jasmin.blanchette at gmail.com
Mon Jun 27 16:07:58 CEST 2011
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" . 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 , and make sure to update "~/.isabelle/etc/components" with the new path (or "~/.isabelle/etc/settings" if you use the "init_component" idiom).
More information about the isabelle-dev