1 For the purposes of the license agreement in the file COPYRIGHT, a
2 'contributor' is anybody who is listed in this file (CONTRIBUTORS) or
3 who is listed as an author in one of the source files of this Isabelle
6 Contributions to Isabelle2011-1
7 -------------------------------
9 * September 2011: Peter Gammie
10 Theory HOL/Libary/Saturated: numbers with saturated arithmetic.
12 * August 2011: Florian Haftmann, Johannes Hölzl and Lars Noschinski, TUM
13 Refined theory on complete lattices.
15 * 2011: Makarius Wenzel, Université Paris-Sud / LRI
16 Various building blocks for Isabelle/Scala layer and Isabelle/jEdit
19 * 2011: Jasmin Blanchette, TUM
20 Various improvements to Sledgehammer, notably: use of sound translations,
21 support for more provers (Waldmeister, LEO-II, Satallax). Further development
25 Contributions to Isabelle2011
26 -----------------------------
28 * January 2011: Stefan Berghofer, secunet Security Networks AG
29 HOL-SPARK: an interactive prover back-end for SPARK.
31 * October 2010: Bogdan Grechuk, University of Edinburgh
32 Extended convex analysis in Multivariate Analysis.
34 * October 2010: Dmitriy Traytel, TUM
35 Coercive subtyping via subtype constraints.
37 * October 2010: Alexander Krauss, TUM
38 Command partial_function for function definitions based on complete
39 partial orders in HOL.
41 * September 2010: Florian Haftmann, TUM
42 Refined concepts for evaluation, i.e., normalization of terms using
45 * September 2010: Florian Haftmann, TUM
46 Code generation for Scala.
48 * August 2010: Johannes Hoelzl, Armin Heller, and Robert Himmelmann, TUM
49 Improved Probability theory in HOL.
51 * July 2010: Florian Haftmann, TUM
52 Reworking and extension of the Imperative HOL framework.
54 * July 2010: Alexander Krauss, TUM and Christian Sternagel, University
56 Ad-hoc overloading. Generic do notation for monads.
59 Contributions to Isabelle2009-2
60 -------------------------------
62 * 2009/2010: Stefan Berghofer, Alexander Krauss, and Andreas Schropp, TUM,
63 Makarius Wenzel, TUM / LRI
64 Elimination of type classes from proof terms.
66 * April 2010: Florian Haftmann, TUM
67 Reorganization of abstract algebra type classes.
69 * April 2010: Florian Haftmann, TUM
70 Code generation for data representations involving invariants;
71 various collections avaiable in theories Fset, Dlist, RBT,
72 Mapping and AssocList.
74 * March 2010: Sascha Boehme, TUM
75 Efficient SHA1 library for Poly/ML.
77 * February 2010: Cezary Kaliszyk and Christian Urban, TUM
78 Quotient type package for Isabelle/HOL.
81 Contributions to Isabelle2009-1
82 -------------------------------
84 * November 2009, Brian Huffman, PSU
85 New definitional domain package for HOLCF.
87 * November 2009: Robert Himmelmann, TUM
88 Derivation and Brouwer's fixpoint theorem in Multivariate Analysis.
90 * November 2009: Stefan Berghofer and Lukas Bulwahn, TUM
91 A tabled implementation of the reflexive transitive closure.
93 * November 2009: Lukas Bulwahn, TUM
94 Predicate Compiler: a compiler for inductive predicates to
95 equational specifications.
97 * November 2009: Sascha Boehme, TUM and Burkhart Wolff, LRI Paris
98 HOL-Boogie: an interactive prover back-end for Boogie and VCC.
100 * October 2009: Jasmin Blanchette, TUM
101 Nitpick: yet another counterexample generator for Isabelle/HOL.
103 * October 2009: Sascha Boehme, TUM
104 Extension of SMT method: proof-reconstruction for the SMT solver Z3.
106 * October 2009: Florian Haftmann, TUM
107 Refinement of parts of the HOL datatype package.
109 * October 2009: Florian Haftmann, TUM
110 Generic term styles for term antiquotations.
112 * September 2009: Thomas Sewell, NICTA
113 More efficient HOL/record implementation.
115 * September 2009: Sascha Boehme, TUM
116 SMT method using external SMT solvers.
118 * September 2009: Florian Haftmann, TUM
119 Refinement of sets and lattices.
121 * July 2009: Jeremy Avigad and Amine Chaieb
124 * July 2009: Philipp Meyer, TUM
125 HOL/Library/Sum_Of_Squares: functionality to call a remote csdp
128 * July 2009: Florian Haftmann, TUM
129 New quickcheck implementation using new code generator.
131 * July 2009: Florian Haftmann, TUM
132 HOL/Library/Fset: an explicit type of sets; finite sets ready to use
135 * June 2009: Florian Haftmann, TUM
136 HOL/Library/Tree: search trees implementing mappings, ready to use
139 * March 2009: Philipp Meyer, TUM
140 Minimization tool for results from Sledgehammer.
143 Contributions to Isabelle2009
144 -----------------------------
146 * March 2009: Robert Himmelmann, TUM and Amine Chaieb, University of
148 Elementary topology in Euclidean space.
150 * March 2009: Johannes Hoelzl, TUM
151 Method "approximation", which proves real valued inequalities by
154 * February 2009: Filip Maric, Univ. of Belgrade
157 * February 2009: Jasmin Christian Blanchette, TUM
158 Misc cleanup of HOL/refute.
160 * February 2009: Timothy Bourke, NICTA
161 New find_consts command.
163 * February 2009: Timothy Bourke, NICTA
164 "solves" criterion for find_theorems and auto_solve option
166 * December 2008: Clemens Ballarin, TUM
167 New locale implementation.
169 * December 2008: Armin Heller, TUM and Alexander Krauss, TUM
170 Method "sizechange" for advanced termination proofs.
172 * November 2008: Timothy Bourke, NICTA
173 Performance improvement (factor 50) for find_theorems.
175 * 2008: Florian Haftmann, TUM
176 Various extensions and restructurings in HOL, improvements
177 in evaluation mechanisms, new module binding.ML for name bindings.
179 * October 2008: Fabian Immler, TUM
180 ATP manager for Sledgehammer, based on ML threads instead of Posix
181 processes. Additional ATP wrappers, including remote SystemOnTPTP
184 * September 2008: Stefan Berghofer, TUM and Marc Bezem, Univ. Bergen
185 Prover for coherent logic.
187 * August 2008: Fabian Immler, TUM
188 Vampire wrapper script for remote SystemOnTPTP service.
191 Contributions to Isabelle2008
192 -----------------------------
195 Alexander Krauss, TUM and Florian Haftmann, TUM and Stefan Berghofer, TUM
196 HOL library improvements.
198 * 2007/2008: Brian Huffman, PSU
199 HOLCF library improvements.
201 * 2007/2008: Stefan Berghofer, TUM
202 HOL-Nominal package improvements.
204 * March 2008: Markus Reiter, TUM
205 HOL/Library/RBT: red-black trees.
207 * February 2008: Alexander Krauss, TUM and Florian Haftmann, TUM and
208 Lukas Bulwahn, TUM and John Matthews, Galois:
209 HOL/Library/Imperative_HOL: Haskell-style imperative data structures
212 * December 2007: Norbert Schirmer, Uni Saarbruecken
213 Misc improvements of record package in HOL.
215 * December 2007: Florian Haftmann, TUM
216 Overloading and class instantiation target.
218 * December 2007: Florian Haftmann, TUM
219 New version of primrec package for local theories.
221 * December 2007: Alexander Krauss, TUM
222 Method "induction_scheme" in HOL.
224 * November 2007: Peter Lammich, Uni Muenster
225 HOL-Lattice: some more lemmas.
228 Contributions to Isabelle2007
229 -----------------------------
231 * October 2007: Norbert Schirmer, TUM / Uni Saarbruecken
232 State Spaces: The Locale Way (in HOL).
234 * October 2007: Mark A. Hillebrand, DFKI
235 Robust sub/superscripts in LaTeX document output.
237 * August 2007: Jeremy Dawson, NICTA and Paul Graunke, Galois and Brian
238 Huffman, PSU and Gerwin Klein, NICTA and John Matthews, Galois
239 HOL-Word: a library for fixed-size machine words in Isabelle.
241 * August 2007: Brian Huffman, PSU
242 HOL/Library/Boolean_Algebra and HOL/Library/Numeral_Type.
244 * June 2007: Amine Chaieb, TUM
245 Semiring normalization and Groebner Bases.
246 Support for dense linear orders.
248 * June 2007: Joe Hurd, Oxford
249 Metis theorem-prover.
251 * 2007: Kong W. Susanto, Cambridge
252 HOL: Metis prover integration.
254 * 2007: Stefan Berghofer, TUM
255 HOL: inductive predicates and sets.
257 * 2007: Norbert Schirmer, TUM
258 HOL/record: misc improvements.
260 * 2006/2007: Alexander Krauss, TUM
261 HOL: function package and related theories on termination.
263 * 2006/2007: Florian Haftmann, TUM
264 Pure: generic code generator framework.
266 HOL: theory reorganization, code generator setup.
268 * 2006/2007: Christian Urban, TUM and Stefan Berghofer, TUM and
270 HOL/Nominal package and related tools.
272 * November 2006: Lukas Bulwahn, TUM
273 HOL: method "lexicographic_order" for function package.
275 * October 2006: Stefan Hohe, TUM
276 HOL-Algebra: ideals and quotients over rings.
278 * August 2006: Amine Chaieb, TUM
279 Experimental support for generic reflection and reification in HOL.
281 * July 2006: Rafal Kolanski, NICTA
282 Hex (0xFF) and binary (0b1011) numerals.
284 * May 2006: Klaus Aehlig, LMU
285 Command 'normal_form': normalization by evaluation.
287 * May 2006: Amine Chaieb, TUM
288 HOL-Complex: Ferrante and Rackoff Algorithm for linear real
291 * February 2006: Benjamin Porter, NICTA
292 HOL and HOL-Complex: generalised mean value theorem, continuum is
293 not denumerable, harmonic and arithmetic series, and denumerability
296 * October 2005: Martin Wildmoser, TUM
297 Sketch for Isar 'guess' element.
300 Contributions to Isabelle2005
301 -----------------------------
303 * September 2005: Lukas Bulwahn and Bernhard Haeupler, TUM
304 HOL-Complex: Formalization of Taylor series.
306 * September 2005: Stephan Merz, Alwen Tiu, QSL Loria
307 Components for SAT solver method using zChaff.
309 * September 2005: Ning Zhang and Christian Urban, LMU Munich
312 * September 2005: Bernhard Haeupler, TUM
313 Method comm_ring for proving equalities in commutative rings.
315 * July/August 2005: Jeremy Avigad, Carnegie Mellon University
316 Various improvements of the HOL and HOL-Complex library.
318 * July 2005: Florian Zuleger, Johannes Hoelzl, and Simon Funke, TUM
319 Some structured proofs about completeness of real numbers.
321 * May 2005: Rafal Kolanski and Gerwin Klein, NICTA
322 Improved retrieval of facts from theory/proof context.
324 * February 2005: Lucas Dixon, University of Edinburgh
325 Improved subst method.
327 * 2005: Brian Huffman, OGI
328 Various improvements of HOLCF.
329 Some improvements of the HOL-Complex library.
331 * 2005: Claire Quigley and Jia Meng, University of Cambridge
332 Some support for asynchronous communication with external provers
335 * 2005: Florian Haftmann, TUM
336 Contributions to document 'sugar'.
337 Various ML combinators, notably linear functional transformations.
338 Some cleanup of ML legacy.
339 Additional antiquotations.
340 Improved Isabelle web site.
342 * 2004/2005: David Aspinall, University of Edinburgh
343 Various elements of XML and PGIP based communication with user
344 interfaces (experimental).
346 * 2004/2005: Gerwin Klein, NICTA
347 Contributions to document 'sugar'.
348 Improved Isabelle web site.
349 Improved HTML presentation of theories.
351 * 2004/2005: Clemens Ballarin, TUM
352 Provers: tools for transitive relations and quasi orders.
353 Improved version of locales, notably interpretation of locales.
354 Improved version of HOL-Algebra.
356 * 2004/2005: Amine Chaieb, TUM
357 Improved version of HOL presburger method.
359 * 2004/2005: Steven Obua, TUM
360 Improved version of HOL/Import, support for HOL-Light.
361 Improved version of HOL-Complex-Matrix.
362 Pure/defs: more sophisticated checks on well-formedness of overloading.
363 Pure/Tools: an experimental evaluator for lambda terms.
365 * 2004/2005: Norbert Schirmer, TUM
366 Contributions to document 'sugar'.
367 Improved version of HOL/record.
369 * 2004/2005: Sebastian Skalberg, TUM
370 Improved version of HOL/Import.
371 Some internal ML reorganizations.
373 * 2004/2005: Tjark Weber, TUM
374 SAT solver method using zChaff.
375 Improved version of HOL/refute.