4 |
4 |
5 |
5 |
6 Contributions to Isabelle2016-1 |
6 Contributions to Isabelle2016-1 |
7 ------------------------------- |
7 ------------------------------- |
8 |
8 |
9 * January 2016: Florian Haftmann, TUM |
9 * October 2016: Jasmin Blanchette |
10 Abolition of compound operators INFIMUM and SUPREMUM |
10 Integration of Nunchaku model finder. |
11 for complete lattices. |
11 |
|
12 * October 2016: Jaime Mendizabal Roche, TUM |
|
13 Ported remaining theories of session Old_Number_Theory to the new |
|
14 Number_Theory and removed Old_Number_Theory. |
|
15 |
|
16 * September 2016: Sascha Boehme |
|
17 Proof method "argo" based on SMT technology for a combination of |
|
18 quantifier-free propositional logic, equality and linear real arithmetic |
|
19 |
|
20 * July 2016: Daniel Stuewe |
|
21 Height-size proofs in HOL-Data_Structures. |
|
22 |
|
23 * July 2016: Manuel Eberl, TUM |
|
24 Algebraic foundation for primes; generalization from nat to general |
|
25 factorial rings. |
|
26 |
|
27 * June 2016: Andreas Lochbihler, ETH Zurich |
|
28 Formalisation of discrete subprobability distributions. |
|
29 |
|
30 * June 2016: Florian Haftmann, TUM |
|
31 Improvements to code generation: optional timing measurements, more succint |
|
32 closures for static evaluation, less ambiguities concering Scala implicits. |
|
33 |
|
34 * May 2016: Manuel Eberl, TUM |
|
35 Code generation for Probability Mass Functions. |
12 |
36 |
13 * March 2016: Florian Haftmann, TUM |
37 * March 2016: Florian Haftmann, TUM |
14 Abstract factorial rings with unique factorization. |
38 Abstract factorial rings with unique factorization. |
15 |
39 |
16 * March 2016: Florian Haftmann, TUM |
40 * March 2016: Florian Haftmann, TUM |
17 Reworking of the HOL char type as special case of a |
41 Reworking of the HOL char type as special case of a finite numeral type. |
18 finite numeral type. |
42 |
19 |
43 * March 2016: Andreas Lochbihler, ETH Zurich |
20 * March 2016: Andreas Lochbihler |
44 Reasoning support for monotonicity, continuity and admissibility in |
21 Reasoning support for monotonicity, continuity and |
45 chain-complete partial orders. |
22 admissibility in chain-complete partial orders. |
46 |
23 |
47 * February - October 2016: Makarius Wenzel |
24 * May 2016: Manuel Eberl |
48 Prover IDE improvements. |
25 Code generation for Probability Mass Functions. |
49 ML IDE improvements: bootstrap of Pure. |
26 |
50 Isar language consolidation. |
27 * June 2016: Andreas Lochbihler |
51 Notational modernization of HOL. |
28 Formalisation of discrete subprobability distributions. |
52 Tight Poly/ML integration. |
29 |
53 More Isabelle/Scala system programming modules (e.g. SSH, Mercurial). |
30 * June 2016: Florian Haftmann, TUM |
54 |
31 Improvements to code generation: optional timing measurements, |
55 * January 2016: Florian Haftmann, TUM |
32 more succint closures for static evaluation, less ambiguities |
56 Abolition of compound operators INFIMUM and SUPREMUM for complete lattices. |
33 concering Scala implicits. |
|
34 |
|
35 * July 2016: Daniel Stuewe |
|
36 Height-size proofs in HOL/Data_Structures |
|
37 |
|
38 * July 2016: Manuel Eberl |
|
39 Algebraic foundation for primes; generalization from nat |
|
40 to general factorial rings |
|
41 |
|
42 * September 2016: Sascha Boehme |
|
43 Proof method 'argo' based on SMT technology for a combination of |
|
44 quantifier-free propositional logic, equality and linear real |
|
45 arithmetic |
|
46 |
|
47 * October 2016: Jaime Mendizabal Roche |
|
48 Ported remaining theories of Old_Number_Theory to the new |
|
49 Number_Theory and removed Old_Number_Theory. |
|
50 |
|
51 * October 2016: Jasmin Blanchette |
|
52 Integration of Nunchaku model finder. |
|
53 |
57 |
54 |
58 |
55 Contributions to Isabelle2016 |
59 Contributions to Isabelle2016 |
56 ----------------------------- |
60 ----------------------------- |
57 |
61 |