|
1 |
|
2 Contributions to Isabelle 2005 |
|
3 ------------------------------ |
1 |
4 |
2 * September 2005: Bernhard Haeupler |
5 * September 2005: Bernhard Haeupler |
3 Method comm_ring for proving equalities in commutative rings. |
6 Method comm_ring for proving equalities in commutative rings. |
4 |
7 |
5 * July 2005: Jeremy Avigad, Carnegie Mellon University |
8 * July/August 2005: Jeremy Avigad, Carnegie Mellon University |
6 Various improvements of the HOL and HOL-Complex library. |
9 Various improvements of the HOL and HOL-Complex library. |
7 |
|
8 * July 2005: Florian Haftmann, TUM |
|
9 Some combinators for linear functional transformations in ML: |
|
10 |-> #-> fold_map etc. |
|
11 |
10 |
12 * July 2005: Florian Zuleger, Johannes Hoelzl, and Simon Funke, TUM |
11 * July 2005: Florian Zuleger, Johannes Hoelzl, and Simon Funke, TUM |
13 Some structured proofs about completeness of real numbers. |
12 Some structured proofs about completeness of real numbers. |
14 |
13 |
15 * May 2005: Rafal Kolanski, NICTA |
14 * May 2005: Rafal Kolanski and Gerwin Klein, NICTA |
16 Substantially improved retrieval of facts from theory/proof context. |
15 Improved retrieval of facts from theory/proof context. |
17 |
|
18 * May 2005: Florian Haftmann, TUM |
|
19 Several new antiquotation. |
|
20 |
16 |
21 * February 2005: Lucas Dixon, University of Edinburgh |
17 * February 2005: Lucas Dixon, University of Edinburgh |
22 Substantially improved subst method. |
18 Improved subst method. |
|
19 |
|
20 * 2005: Brian Huffman, OGI |
|
21 Various improvements of HOLCF. |
|
22 Some improvements of the HOL-Complex library. |
|
23 |
|
24 * 2005: Claire Quigley and Jia Meng, University of Cambridge |
|
25 Some support for asynchronous communication with external provers |
|
26 (experimental). |
|
27 |
|
28 * 2005: Florian Haftmann, TUM |
|
29 Various ML combinators, notably linear functional transformations. |
|
30 Some cleanup of ML legacy. |
|
31 Additional antiquotations. |
|
32 Improved Isabelle web site. |
|
33 |
|
34 * 2004/2005: David Aspinall, University of Edinburgh |
|
35 Various elements of XML and PGIP based communication with user |
|
36 interfaces (experimental). |
|
37 |
|
38 * 2004/2005: Gerwin Klein, NICTA |
|
39 Contributions to document 'sugar'. |
|
40 Improved Isabelle web site. |
|
41 Improved HTML presentation of theories. |
|
42 |
|
43 * 2004/2005: Clemens Ballarin, TUM |
|
44 Provers: tools for transitive relations and quasi orders. |
|
45 Improved version of locales, notably interpretation of locales. |
|
46 Improved version of HOL-Algebra. |
|
47 |
|
48 * 2004/2005: Amine Chaieb, TUM |
|
49 Improved version of HOL presburger method. |
|
50 |
|
51 * 2004/2005: Steven Obua, TUM |
|
52 Pure/defs: more sophisticated check on well-formedness of overloading. |
|
53 Improved version of HOL/Import, support for HOL-Light. |
|
54 Improved version of HOL-Complex-Matrix. |
|
55 |
|
56 * 2004/2005: Norbert Schirmer, TUM |
|
57 Contributions to document 'sugar'. |
|
58 Improved version of HOL/record. |
|
59 |
|
60 * 2004/2005: Sebastian Skalberg, TUM |
|
61 Improved version of HOL/Import. |
|
62 Some internal ML reorganizations. |
|
63 |
|
64 * 2004/2005: Tjark Weber, TUM |
|
65 Improved version of HOL/refute. |
23 |
66 |
24 $Id$ |
67 $Id$ |