4 |
4 |
5 |
5 |
6 Contributions to this Isabelle version |
6 Contributions to this Isabelle version |
7 -------------------------------------- |
7 -------------------------------------- |
8 |
8 |
|
9 * November 2020: Florian Haftmann |
|
10 Bundle mixins for locale and class expressions. |
|
11 |
9 * October 2020: Jasmin Blanchette, Martin Desharnais, Mathias Fleury |
12 * October 2020: Jasmin Blanchette, Martin Desharnais, Mathias Fleury |
10 Use veriT in proof preplay in Sledgehammer. |
13 Use veriT in proof preplay in Sledgehammer. |
11 |
14 |
12 * October 2020: Mathias Fleury |
15 * October 2020: Mathias Fleury |
13 Updated proof reconstruction for the SMT solver veriT in the smt method. |
16 Updated proof reconstruction for the SMT solver veriT in the smt method. |
14 |
17 |
15 * October 2020: Jasmin Blanchette, Martin Desharnais |
18 * October 2020: Jasmin Blanchette, Martin Desharnais |
16 Integration of E 2.5 for Sledgehammer. |
19 Integration of E 2.5 for Sledgehammer. |
17 |
20 |
|
21 * September 2020: Florian Haftmann |
|
22 Substantial reworking and modularization of Word library, with |
|
23 generic type conversions. |
|
24 |
18 * August 2020: Makarius Wenzel |
25 * August 2020: Makarius Wenzel |
19 Improved monitoring of runtime statistics: ML GC progress and Java. |
26 Improved monitoring of runtime statistics: ML GC progress and Java. |
20 |
27 |
21 * July 2020: Martin Desharnais |
28 * July 2020: Martin Desharnais |
22 Integration of Metis 2.4. |
29 Integration of Metis 2.4. |
23 |
30 |
24 * June 2020: Makarius Wenzel |
31 * June 2020: Makarius Wenzel |
25 Batch-builds via "isabelle build" allow to invoke Scala from ML. |
32 Batch-builds via "isabelle build" allow to invoke Scala from ML. |
|
33 |
|
34 * June 2020: Florian Haftmann |
|
35 Simproc defined_all for more aggressive substitution with variables |
|
36 from assumptions. |
26 |
37 |
27 * May 2020: Makarius Wenzel |
38 * May 2020: Makarius Wenzel |
28 Antiquotations for Isabelle systems programming, notably @{scala_function} |
39 Antiquotations for Isabelle systems programming, notably @{scala_function} |
29 and @{scala} to invoke Scala from ML. |
40 and @{scala} to invoke Scala from ML. |
30 |
41 |
31 * May 2020: Florian Haftmann |
42 * May 2020: Florian Haftmann |
32 Generic algebraically founded bit operations NOT, AND, OR, XOR. |
43 Generic algebraically founded bit operations NOT, AND, OR, XOR. |
33 |
|
34 * Sept. 2020: Florian Haftmann |
|
35 Substantial reworking and modularization of Word library, with |
|
36 generic type conversions. |
|
37 |
|
38 * June 2020: Florian Haftmann |
|
39 Simproc defined_all for more aggressive substitution with variables |
|
40 from assumptions. |
|
41 |
44 |
42 |
45 |
43 Contributions to Isabelle2020 |
46 Contributions to Isabelle2020 |
44 ----------------------------- |
47 ----------------------------- |
45 |
48 |