author | huffman |
Sat, 16 Dec 2006 19:37:07 +0100 | |
changeset 21864 | 2ecfd8985982 |
parent 21242 | d73735bb33c1 |
child 22449 | ece6952a8975 |
permissions | -rw-r--r-- |
20340
6afc1c133b86
Amine Chaieb: experimental generic reflection and reification in HOL;
wenzelm
parents:
20067
diff
changeset
|
1 |
|
17866 | 2 |
Contributions to Isabelle |
3 |
------------------------- |
|
4 |
||
21242
d73735bb33c1
* November 2006: Lukas Bulwahn, TUM -- HOL/function: method "lexicographic_order".
wenzelm
parents:
21169
diff
changeset
|
5 |
* November 2006: Lukas Bulwahn, TUM |
d73735bb33c1
* November 2006: Lukas Bulwahn, TUM -- HOL/function: method "lexicographic_order".
wenzelm
parents:
21169
diff
changeset
|
6 |
HOL/function: method "lexicographic_order". |
d73735bb33c1
* November 2006: Lukas Bulwahn, TUM -- HOL/function: method "lexicographic_order".
wenzelm
parents:
21169
diff
changeset
|
7 |
|
21169 | 8 |
* October 2006: Stefan Hohe, TUM |
9 |
HOL-Algebra: ideals and quotients over rings. |
|
10 |
||
20340
6afc1c133b86
Amine Chaieb: experimental generic reflection and reification in HOL;
wenzelm
parents:
20067
diff
changeset
|
11 |
* August 2006: Amine Chaieb, TUM |
6afc1c133b86
Amine Chaieb: experimental generic reflection and reification in HOL;
wenzelm
parents:
20067
diff
changeset
|
12 |
Experimental support for generic reflection and reification in HOL. |
6afc1c133b86
Amine Chaieb: experimental generic reflection and reification in HOL;
wenzelm
parents:
20067
diff
changeset
|
13 |
|
20067
26bac504ef90
hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents:
19896
diff
changeset
|
14 |
* July 2006: Rafal Kolanski, NICTA |
26bac504ef90
hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents:
19896
diff
changeset
|
15 |
Hex (0xFF) and binary (0b1011) numerals. |
26bac504ef90
hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents:
19896
diff
changeset
|
16 |
|
19896 | 17 |
* May 2006: Klaus Aehlig, LMU |
18 |
Command 'normal_form': normalization by evaluation. |
|
19 |
||
19650 | 20 |
* May 2006: Amine Chaieb, TUM |
21 |
HOL-Complex: Ferrante and Rackoff Algorithm for linear real |
|
22 |
arithmetic. |
|
19470 | 23 |
|
24 |
* February 2006: Benjamin Porter, NICTA |
|
25 |
HOL and HOL-Complex: generalied mean value theorem, continuum is |
|
26 |
not denumerable, harmonic and arithmetic series, and denumerability |
|
27 |
of rationals. |
|
17532 | 28 |
|
19650 | 29 |
* October 2005: Martin Wildmoser, TUM |
30 |
Sketch for Isar 'guess' element. |
|
31 |
||
32 |
||
17532 | 33 |
Contributions to Isabelle 2005 |
34 |
------------------------------ |
|
17382 | 35 |
|
17640 | 36 |
* September 2005: Lukas Bulwahn and Bernhard Haeupler, TUM |
37 |
HOL-Complex: Formalization of Taylor series. |
|
38 |
||
39 |
* September 2005: Stephan Merz, Alwen Tiu, QSL Loria |
|
40 |
Components for SAT solver method using zChaff. |
|
41 |
||
17534 | 42 |
* September 2005: Ning Zhang and Christian Urban, LMU Munich |
43 |
A Chinese theory. |
|
44 |
||
17562 | 45 |
* September 2005: Bernhard Haeupler, TUM |
17382 | 46 |
Method comm_ring for proving equalities in commutative rings. |
16892 | 47 |
|
17532 | 48 |
* July/August 2005: Jeremy Avigad, Carnegie Mellon University |
16892 | 49 |
Various improvements of the HOL and HOL-Complex library. |
16868 | 50 |
|
16892 | 51 |
* July 2005: Florian Zuleger, Johannes Hoelzl, and Simon Funke, TUM |
52 |
Some structured proofs about completeness of real numbers. |
|
53 |
||
17532 | 54 |
* May 2005: Rafal Kolanski and Gerwin Klein, NICTA |
55 |
Improved retrieval of facts from theory/proof context. |
|
15994 | 56 |
|
16252 | 57 |
* February 2005: Lucas Dixon, University of Edinburgh |
17532 | 58 |
Improved subst method. |
59 |
||
60 |
* 2005: Brian Huffman, OGI |
|
61 |
Various improvements of HOLCF. |
|
62 |
Some improvements of the HOL-Complex library. |
|
63 |
||
64 |
* 2005: Claire Quigley and Jia Meng, University of Cambridge |
|
65 |
Some support for asynchronous communication with external provers |
|
66 |
(experimental). |
|
67 |
||
68 |
* 2005: Florian Haftmann, TUM |
|
17543 | 69 |
Contributions to document 'sugar'. |
17532 | 70 |
Various ML combinators, notably linear functional transformations. |
71 |
Some cleanup of ML legacy. |
|
72 |
Additional antiquotations. |
|
73 |
Improved Isabelle web site. |
|
74 |
||
75 |
* 2004/2005: David Aspinall, University of Edinburgh |
|
76 |
Various elements of XML and PGIP based communication with user |
|
77 |
interfaces (experimental). |
|
78 |
||
79 |
* 2004/2005: Gerwin Klein, NICTA |
|
80 |
Contributions to document 'sugar'. |
|
81 |
Improved Isabelle web site. |
|
82 |
Improved HTML presentation of theories. |
|
83 |
||
84 |
* 2004/2005: Clemens Ballarin, TUM |
|
85 |
Provers: tools for transitive relations and quasi orders. |
|
86 |
Improved version of locales, notably interpretation of locales. |
|
87 |
Improved version of HOL-Algebra. |
|
88 |
||
89 |
* 2004/2005: Amine Chaieb, TUM |
|
90 |
Improved version of HOL presburger method. |
|
91 |
||
92 |
* 2004/2005: Steven Obua, TUM |
|
93 |
Improved version of HOL/Import, support for HOL-Light. |
|
94 |
Improved version of HOL-Complex-Matrix. |
|
17572 | 95 |
Pure/defs: more sophisticated checks on well-formedness of overloading. |
17543 | 96 |
Pure/Tools: an experimental evaluator for lambda terms. |
17532 | 97 |
|
98 |
* 2004/2005: Norbert Schirmer, TUM |
|
99 |
Contributions to document 'sugar'. |
|
100 |
Improved version of HOL/record. |
|
101 |
||
102 |
* 2004/2005: Sebastian Skalberg, TUM |
|
103 |
Improved version of HOL/Import. |
|
104 |
Some internal ML reorganizations. |
|
105 |
||
106 |
* 2004/2005: Tjark Weber, TUM |
|
17640 | 107 |
SAT solver method using zChaff. |
17532 | 108 |
Improved version of HOL/refute. |
16252 | 109 |
|
15994 | 110 |
$Id$ |