CONTRIBUTORS
2010-09-23 haftmann 2010-09-23 CONTRIBUTORS and NEWS
2010-08-23 hoelzl 2010-08-23 Rewrite the Probability theory. Introduced pinfreal as real numbers with infinity. Use pinfreal as value for measures. Introduces Lebesgue Measure based on the integral in Multivariate Analysis. Proved Radon Nikodym for arbitrary sigma finite measure spaces.
2010-08-17 haftmann 2010-08-17 NEWS and CONTRIBUTORS
2010-06-07 wenzelm 2010-06-07 back to non-release mode;
2010-06-03 krauss 2010-06-03 CONTRIBUTORS
2010-06-02 wenzelm 2010-06-02 more CONTRIBUTORS;
2010-05-27 wenzelm 2010-05-27 misc updates for release;
2010-04-27 haftmann 2010-04-27 NEWS and CONTRIBUTORS
2009-12-04 wenzelm 2009-12-04 back to after-release mode;
2009-11-25 wenzelm 2009-11-25 tuned affiliation;
2009-11-25 boehmes 2009-11-25 extended list of HOL-Boogie contributors
2009-11-23 haftmann 2009-11-23 CONTRIBUTORS
2009-11-22 wenzelm 2009-11-22 more NEWS, more tuning for release;
2009-11-22 wenzelm 2009-11-22 misc tuning and updates for official release;
2009-11-19 hoelzl 2009-11-19 Added the contributions of Robert Himmelmann to CONTRIBUTIONS and NEWS
2009-11-12 bulwahn 2009-11-12 added a tabled implementation of the reflexive transitive closure
2009-11-12 bulwahn 2009-11-12 announcing the predicate compiler in NEWS and CONTRIBUTORS
2009-11-03 boehmes 2009-11-03 added HOL-Boogie
2009-10-26 blanchet 2009-10-26 merged
2009-10-22 blanchet 2009-10-22 added Nitpick's theory and ML files to Isabelle/HOL; the examples and the documentation are on their way.
2009-10-26 wenzelm 2009-10-26 misc tuning and updates;
2009-10-20 boehmes 2009-10-20 added proof reconstructon for Z3, added certificates for simpler re-checking of proofs (no need to invoke external solvers), added examples and certificates for all examples, removed Unsynchronized.ref (in smt_normalize.ML)
2009-10-19 haftmann 2009-10-19 CONTRIBUTORS
2009-09-29 wenzelm 2009-09-29 Thomas Sewell, NICTA: more efficient HOL/record implementation;
2009-09-18 boehmes 2009-09-18 added new method "smt": an oracle-based connection to external SMT solvers
2009-09-18 haftmann 2009-09-18 tuned NEWS, added CONTRIBUTORS
2009-07-24 Philipp Meyer 2009-07-24 Functionality for sum of squares to call a remote csdp prover
2009-07-14 haftmann 2009-07-14 NEWS and CONTRIBUTORS
2009-06-05 haftmann 2009-06-05 CONTRIBUTORS
2009-04-25 wenzelm 2009-04-25 post Isabelle2009 version;
2009-04-08 wenzelm 2009-04-08 updated official title of contribution by Johannes Hoelzl;
2009-03-09 wenzelm 2009-03-09 more contributors;
2009-02-28 wenzelm 2009-02-28 A Serbian theory, by Filip Maric.
2009-02-28 wenzelm 2009-02-28 more CONTRIBUTORS; fixed some dates;
2009-02-27 wenzelm 2009-02-27 more CONTRIBUTORS;
2009-02-13 kleing 2009-02-13 added find_consts to NEWS and CONTRIBUTORS
2009-02-11 kleing 2009-02-11 updated NEWS etc with "solves" criterion and auto_solves
2009-01-08 haftmann 2009-01-08 NEWS and CONTRIBUTORS
2008-12-27 krauss 2008-12-27 tuned NEWS; CONTRIBUTORS
2008-12-20 wenzelm 2008-12-20 removed Ids;
2008-11-28 kleing 2008-11-28 added Tim's find_theorems performance patch
2008-10-15 wenzelm 2008-10-15 generic ATP manager based on threads (by Fabian Immler);
2008-10-03 wenzelm 2008-10-03 Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
2008-05-28 wenzelm 2008-05-28 more contribs;
2008-05-12 wenzelm 2008-05-12 misc tuning;
2008-04-22 haftmann 2008-04-22 added entries
2008-03-05 wenzelm 2008-03-05 HOL/Library/RBT.thy;
2007-11-26 wenzelm 2007-11-26 Peter Lammich: HOL-Lattice lemmas;
2007-11-21 wenzelm 2007-11-21 tuned;
2007-11-20 wenzelm 2007-11-20 tuned;
2007-11-12 schirmer 2007-11-12 fixed typo;
2007-11-11 wenzelm 2007-11-11 HOL-Statespace;
2007-10-16 wenzelm 2007-10-16 Mark A. Hillebrand, DFKI: Robust sub/superscripts in LaTeX document output.
2007-10-01 wenzelm 2007-10-01 Norbert Schirmer: record improvements;
2007-10-01 wenzelm 2007-10-01 misc tuning and update;
2007-08-20 kleing 2007-08-20 * HOL-Word: New extensive library and type for generic, fixed size machine words, with arithemtic, bit-wise, shifting and rotating operations, reflection into int, nat, and bool lists, automation for linear arithmetic (by automatic reflection into nat or int), including lemmas on overflow and monotonicity. Instantiated to all appropriate arithmetic type classes, supporting automatic simplification of numerals on all operations. Jointly developed by NICTA, Galois, and PSU. * still to do: README.html/document + moving some of the generic lemmas to appropriate place in distribution
2007-08-20 kleing 2007-08-20 boolean algebras as locales and numbers as types by Brian Huffman
2007-06-21 paulson 2007-06-21 integration of Metis prover
2007-06-14 kleing 2007-06-14 clarified who we consider to be a contributor
2007-06-05 wenzelm 2007-06-05 Semiring normalization and Groebner Bases.