equal
deleted
inserted
replaced
4 |
4 |
5 |
5 |
6 Contributions to this Isabelle version |
6 Contributions to this Isabelle version |
7 -------------------------------------- |
7 -------------------------------------- |
8 |
8 |
|
9 * January 2019: Florian Haftmann |
|
10 Clarified syntax and congruence rules for big operators on sets |
|
11 involving the image operator. |
|
12 |
|
13 * January 2919: Florian Haftmann |
|
14 Renovation of code generation, particularly proper strings for OCaml |
|
15 end export into session data. |
|
16 |
9 * February 2019: Jeremy Sylvestre |
17 * February 2019: Jeremy Sylvestre |
10 Formal Laurent Series and overhaul of Formal power series. |
18 Formal Laurent Series and overhaul of Formal power series. |
11 |
19 |
12 * February 2019: Manuel Eberl |
20 * February 2019: Manuel Eberl |
13 Exponentiation by squaring, used to implement "power" in monoid_mult and |
21 Exponentiation by squaring, used to implement "power" in monoid_mult and |
19 |
27 |
20 * January 2019: Andreas Lochbihler |
28 * January 2019: Andreas Lochbihler |
21 New implementation for case_of_simps based on Code_Lazy's |
29 New implementation for case_of_simps based on Code_Lazy's |
22 pattern matching elimination algorithm. |
30 pattern matching elimination algorithm. |
23 |
31 |
|
32 * December 2018: Florian Haftmann |
|
33 Generic executable sorting algorithms based on executable comparators. |
|
34 |
24 * October 2018: Mathias Fleury |
35 * October 2018: Mathias Fleury |
25 Proof reconstruction for the SMT solver veriT in the smt method |
36 Proof reconstruction for the SMT solver veriT in the smt method. |
26 |
37 |
27 |
38 |
28 Contributions to Isabelle2018 |
39 Contributions to Isabelle2018 |
29 ----------------------------- |
40 ----------------------------- |
30 |
41 |