17 * Summer 2014: Florian Haftmann, TUM |
17 * Summer 2014: Florian Haftmann, TUM |
18 Consolidation and generalization of facts concerning (abelian) |
18 Consolidation and generalization of facts concerning (abelian) |
19 semigroups and monoids, particularly products (resp. sums) on |
19 semigroups and monoids, particularly products (resp. sums) on |
20 finite sets. |
20 finite sets. |
21 |
21 |
22 * June 2014: Florian Haftmann, TUM |
|
23 Internal reorganisation of the local theory / named target stack. |
|
24 |
|
25 * Summer 2014: Mathias Fleury, ENS Rennes, and Albert Steckermeier, TUM |
22 * Summer 2014: Mathias Fleury, ENS Rennes, and Albert Steckermeier, TUM |
26 Work on exotic automatic theorem provers for Sledgehammer (LEO-II, |
23 Work on exotic automatic theorem provers for Sledgehammer (LEO-II, |
27 veriT, Waldmeister, etc.). |
24 veriT, Waldmeister, etc.). |
28 |
25 |
|
26 * June 2014: Florian Haftmann, TUM |
|
27 Internal reorganisation of the local theory / named target stack. |
|
28 |
29 * June 2014: Sudeep Kanav, TUM, Jeremy Avigad, CMU, and Johannes Hölzl, TUM |
29 * June 2014: Sudeep Kanav, TUM, Jeremy Avigad, CMU, and Johannes Hölzl, TUM |
30 Various properties of exponentially, Erlang, and normal distributed |
30 Various properties of exponentially, Erlang, and normal distributed |
31 random variables. |
31 random variables. |
32 |
32 |
33 * May 2014: Cezary Kaliszyk, University of Innsbruck, and |
33 * May 2014: Cezary Kaliszyk, University of Innsbruck, and |
41 Permanent interpretation inside theory, locale and class targets |
41 Permanent interpretation inside theory, locale and class targets |
42 with mixin definitions. |
42 with mixin definitions. |
43 |
43 |
44 * Spring 2014: Lawrence C Paulson, Cambridge |
44 * Spring 2014: Lawrence C Paulson, Cambridge |
45 Theory Complex_Basic_Analysis. Tidying up Number_Theory vs Old_Number_Theory |
45 Theory Complex_Basic_Analysis. Tidying up Number_Theory vs Old_Number_Theory |
|
46 |
|
47 * Winter 2013 and Spring 2014: Ondrej Kuncar, TUM |
|
48 Various improvements to Lifting/Transfer, integration with the BNF package. |
46 |
49 |
47 * Winter 2013 and Spring 2014: Makarius Wenzel, Université Paris-Sud / LRI |
50 * Winter 2013 and Spring 2014: Makarius Wenzel, Université Paris-Sud / LRI |
48 Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE. |
51 Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE. |
49 |
52 |
50 * Fall 2013 and Winter 2014: Martin Desharnais, Lorenz Panny, |
53 * Fall 2013 and Winter 2014: Martin Desharnais, Lorenz Panny, |