equal
deleted
inserted
replaced
5 |
5 |
6 |
6 |
7 Contributions to this Isabelle version |
7 Contributions to this Isabelle version |
8 -------------------------------------- |
8 -------------------------------------- |
9 |
9 |
|
10 * July 2009: Philipp Meyer, TUM |
|
11 HOL/Library/Sum_of_Squares: functionality to call a remote csdp prover |
|
12 |
10 * July 2009: Florian Haftmann, TUM |
13 * July 2009: Florian Haftmann, TUM |
11 New quickcheck implementation using new code generator |
14 New quickcheck implementation using new code generator |
12 |
15 |
13 * July 2009: Florian Haftmann, TUM |
16 * July 2009: Florian Haftmann, TUM |
14 HOL/Library/FSet: an explicit type of sets; finite sets ready to use for code generation |
17 HOL/Library/FSet: an explicit type of sets; finite sets ready to use for code generation |
16 * June 2009: Andreas Lochbihler, Uni Karlsruhe |
19 * June 2009: Andreas Lochbihler, Uni Karlsruhe |
17 HOL/Library/Fin_Fun: almost everywhere constant functions |
20 HOL/Library/Fin_Fun: almost everywhere constant functions |
18 |
21 |
19 * June 2009: Florian Haftmann, TUM |
22 * June 2009: Florian Haftmann, TUM |
20 HOL/Library/Tree: searchtrees implementing mappings, ready to use for code generation |
23 HOL/Library/Tree: searchtrees implementing mappings, ready to use for code generation |
|
24 |
|
25 * March 2009: Philipp Meyer, TUM |
|
26 minimalization algorithm for results from sledgehammer call |
21 |
27 |
22 Contributions to Isabelle2009 |
28 Contributions to Isabelle2009 |
23 ----------------------------- |
29 ----------------------------- |
24 |
30 |
25 * March 2009: Robert Himmelmann, TUM and Amine Chaieb, University of |
31 * March 2009: Robert Himmelmann, TUM and Amine Chaieb, University of |