5 |
5 |
6 Contributions to Isabelle2012 |
6 Contributions to Isabelle2012 |
7 ----------------------------- |
7 ----------------------------- |
8 |
8 |
9 * April 2012: Johannes Hölzl, TUM |
9 * April 2012: Johannes Hölzl, TUM |
10 Probability: Introduced type to represent measures instead of locales. |
10 Probability: Introduced type to represent measures instead of |
|
11 locales. |
11 |
12 |
12 * April 2012: Johannes Hölzl, Fabian Immler, TUM |
13 * April 2012: Johannes Hölzl, Fabian Immler, TUM |
13 Float: Moved to Dyadic rationals to represent floating point numers. |
14 Float: Moved to Dyadic rationals to represent floating point numers. |
14 |
15 |
15 * April 2012: Thomas Sewell, NICTA |
16 * April 2012: Thomas Sewell, NICTA and |
16 (based on work done with Sascha Boehme, TUM in 2010) |
17 2010: Sascha Boehme, TUM |
17 WordBitwise: logic/circuit expansion of bitvector equalities/inequalities. |
18 Theory HOL/Word/WordBitwise: logic/circuit expansion of bitvector |
18 |
19 equalities/inequalities. |
19 * March 2012: Christian Sternagel, Japan Advanced Institute of Science |
20 |
20 and Technology |
21 * March 2012: Christian Sternagel, JAIST |
21 Consolidated theory of relation composition. |
22 Consolidated theory of relation composition. |
22 |
23 |
23 * March 2012: Nik Sultana, University of Cambridge |
24 * March 2012: Nik Sultana, University of Cambridge |
24 HOL/TPTP parser and import facilities. |
25 HOL/TPTP parser and import facilities. |
25 |
26 |
29 |
30 |
30 * January 2012: Florian Haftmann, TUM, et al. |
31 * January 2012: Florian Haftmann, TUM, et al. |
31 (Re-)Introduction of the "set" type constructor. |
32 (Re-)Introduction of the "set" type constructor. |
32 |
33 |
33 * 2012: Ondrej Kuncar, TUM |
34 * 2012: Ondrej Kuncar, TUM |
34 New package Lifting, various improvements and refinements to the Quotient package. |
35 New package Lifting, various improvements and refinements to the |
|
36 Quotient package. |
35 |
37 |
36 * 2011/2012: Jasmin Blanchette, TUM |
38 * 2011/2012: Jasmin Blanchette, TUM |
37 Various improvements to Sledgehammer, notably: tighter integration |
39 Various improvements to Sledgehammer, notably: tighter integration |
38 with SPASS, support for more provers (Alt-Ergo, iProver, iProver-Eq). |
40 with SPASS, support for more provers (Alt-Ergo, iProver, |
|
41 iProver-Eq). |
39 |
42 |
40 * 2011/2012: Makarius Wenzel, Université Paris-Sud / LRI |
43 * 2011/2012: Makarius Wenzel, Université Paris-Sud / LRI |
41 Various refinements of local theory infrastructure. |
44 Various refinements of local theory infrastructure. |
42 Improvements of Isabelle/Scala layer and Isabelle/jEdit Prover IDE. |
45 Improvements of Isabelle/Scala layer and Isabelle/jEdit Prover IDE. |
43 |
46 |