4 distribution. |
4 distribution. |
5 |
5 |
6 Contributions to this Isabelle version |
6 Contributions to this Isabelle version |
7 -------------------------------------- |
7 -------------------------------------- |
8 |
8 |
|
9 * Summer 2014: Mathias Fleury, ENS Rennes, and Albert Steckermeier, TUM |
|
10 Work on exotic automatic theorem provers for Sledgehammer (LEO-II, veriT, |
|
11 Waldmeister, etc.). |
|
12 |
9 * May 2014: Cezary Kaliszyk, University of Innsbruck, and Jasmin Blanchette, TUM |
13 * May 2014: Cezary Kaliszyk, University of Innsbruck, and Jasmin Blanchette, TUM |
10 SML-based engines for MaSh. |
14 SML-based engines for MaSh. |
11 |
15 |
12 * March 2014: René Thiemann |
16 * March 2014: René Thiemann |
13 Improved code generation for multisets. |
17 Improved code generation for multisets. |
14 |
18 |
15 * February 2014: Florian Haftmann, TUM |
19 * February 2014: Florian Haftmann, TUM |
16 Permanent interpretation inside theory, locale and class targets with mixin definitions. |
20 Permanent interpretation inside theory, locale and class targets with mixin definitions. |
17 |
21 |
18 * Fall 2013 and Winter 2014: Lorenz Panny, Dmitriy Traytel, and |
22 * Fall 2013 and Winter 2014: Martin Desharnais, Lorenz Panny, Dmitriy Traytel, |
19 Jasmin Blanchette, TUM |
23 and Jasmin Blanchette, TUM |
20 Various improvements to the BNF-based (co)datatype package, including |
24 Various improvements to the BNF-based (co)datatype package, including |
21 a more polished "primcorec" command, optimizations, and integration in |
25 a more polished "primcorec" command, optimizations, and integration in |
22 the "HOL" session. |
26 the "HOL" session. |
23 |
27 |
24 * Winter/Spring 2014: Sascha Boehme, QAware GmbH, and Jasmin Blanchette, TUM |
28 * Winter/Spring 2014: Sascha Boehme, QAware GmbH, and Jasmin Blanchette, TUM |