50 Isar language consolidation. |
50 Isar language consolidation. |
51 Notational modernization of HOL. |
51 Notational modernization of HOL. |
52 Tight Poly/ML integration. |
52 Tight Poly/ML integration. |
53 More Isabelle/Scala system programming modules (e.g. SSH, Mercurial). |
53 More Isabelle/Scala system programming modules (e.g. SSH, Mercurial). |
54 |
54 |
55 * January 2016: Florian Haftmann, TUM |
|
56 Abolition of compound operators INFIMUM and SUPREMUM for complete lattices. |
|
57 |
|
58 |
|
59 Contributions to Isabelle2016 |
|
60 ----------------------------- |
|
61 |
|
62 * Winter 2016: Jasmin Blanchette, Inria & LORIA & MPII, Aymeric Bouzy, |
55 * Winter 2016: Jasmin Blanchette, Inria & LORIA & MPII, Aymeric Bouzy, |
63 Ecole polytechnique, Andreas Lochbihler, ETH Zurich, Andrei Popescu, |
56 Ecole polytechnique, Andreas Lochbihler, ETH Zurich, Andrei Popescu, |
64 Middlesex University, and Dmitriy Traytel, ETH Zurich |
57 Middlesex University, and Dmitriy Traytel, ETH Zurich |
65 'corec' command and friends. |
58 'corec' command and friends. |
|
59 |
|
60 * January 2016: Florian Haftmann, TUM |
|
61 Abolition of compound operators INFIMUM and SUPREMUM for complete lattices. |
|
62 |
|
63 |
|
64 Contributions to Isabelle2016 |
|
65 ----------------------------- |
66 |
66 |
67 * Winter 2016: Manuel Eberl, TUM |
67 * Winter 2016: Manuel Eberl, TUM |
68 Support for real exponentiation ("powr") in the "approximation" method. |
68 Support for real exponentiation ("powr") in the "approximation" method. |
69 (This was removed in Isabelle 2015 due to a changed definition of "powr".) |
69 (This was removed in Isabelle 2015 due to a changed definition of "powr".) |
70 |
70 |