6 |
6 |
7 Contributions to this Isabelle version |
7 Contributions to this Isabelle version |
8 -------------------------------------- |
8 -------------------------------------- |
9 |
9 |
10 * October 2009: Sascha Boehme, TUM |
10 * October 2009: Sascha Boehme, TUM |
11 Extension of SMT method: proof-reconstruction for the SMT solver Z3 |
11 Extension of SMT method: proof-reconstruction for the SMT solver Z3. |
12 |
12 |
13 * October 2009: Florian Haftmann, TUM |
13 * October 2009: Florian Haftmann, TUM |
14 Refinement of parts of the HOL datatype package |
14 Refinement of parts of the HOL datatype package. |
15 |
15 |
16 * October 2009: Florian Haftmann, TUM |
16 * October 2009: Florian Haftmann, TUM |
17 Generic term styles for term antiquotations |
17 Generic term styles for term antiquotations. |
18 |
18 |
19 * September 2009: Thomas Sewell, NICTA |
19 * September 2009: Thomas Sewell, NICTA |
20 More efficient HOL/record implementation |
20 More efficient HOL/record implementation. |
21 |
21 |
22 * September 2009: Sascha Boehme, TUM |
22 * September 2009: Sascha Boehme, TUM |
23 SMT method using external SMT solvers |
23 SMT method using external SMT solvers. |
24 |
24 |
25 * September 2009: Florian Haftmann, TUM |
25 * September 2009: Florian Haftmann, TUM |
26 Refinement of sets and lattices |
26 Refinement of sets and lattices. |
27 |
27 |
28 * July 2009: Jeremy Avigad and Amine Chaieb |
28 * July 2009: Jeremy Avigad and Amine Chaieb |
29 New number theory |
29 New number theory. |
30 |
30 |
31 * July 2009: Philipp Meyer, TUM |
31 * July 2009: Philipp Meyer, TUM |
32 HOL/Library/Sum_of_Squares: functionality to call a remote csdp prover |
32 HOL/Library/Sum_Of_Squares: functionality to call a remote csdp |
|
33 prover. |
33 |
34 |
34 * July 2009: Florian Haftmann, TUM |
35 * July 2009: Florian Haftmann, TUM |
35 New quickcheck implementation using new code generator |
36 New quickcheck implementation using new code generator. |
36 |
37 |
37 * July 2009: Florian Haftmann, TUM |
38 * July 2009: Florian Haftmann, TUM |
38 HOL/Library/FSet: an explicit type of sets; finite sets ready to use for code generation |
39 HOL/Library/FSet: an explicit type of sets; finite sets ready to use |
39 |
40 for code generation. |
40 * June 2009: Andreas Lochbihler, Uni Karlsruhe |
|
41 HOL/Library/Fin_Fun: almost everywhere constant functions |
|
42 |
41 |
43 * June 2009: Florian Haftmann, TUM |
42 * June 2009: Florian Haftmann, TUM |
44 HOL/Library/Tree: searchtrees implementing mappings, ready to use for code generation |
43 HOL/Library/Tree: searchtrees implementing mappings, ready to use |
|
44 for code generation. |
45 |
45 |
46 * March 2009: Philipp Meyer, TUM |
46 * March 2009: Philipp Meyer, TUM |
47 minimalization algorithm for results from sledgehammer call |
47 Minimalization algorithm for results from sledgehammer call. |
|
48 |
48 |
49 |
49 Contributions to Isabelle2009 |
50 Contributions to Isabelle2009 |
50 ----------------------------- |
51 ----------------------------- |
51 |
52 |
52 * March 2009: Robert Himmelmann, TUM and Amine Chaieb, University of |
53 * March 2009: Robert Himmelmann, TUM and Amine Chaieb, University of |