1.1 --- a/CONTRIBUTORS	Mon Oct 26 11:37:33 2009 +0100
     1.2 +++ b/CONTRIBUTORS	Mon Oct 26 11:57:58 2009 +0100
     1.3 @@ -8,43 +8,44 @@
     1.4  --------------------------------------
     1.5  
     1.6  * October 2009: Sascha Boehme, TUM
     1.7 -  Extension of SMT method: proof-reconstruction for the SMT solver Z3
     1.8 +  Extension of SMT method: proof-reconstruction for the SMT solver Z3.
     1.9  
    1.10  * October 2009: Florian Haftmann, TUM
    1.11 -  Refinement of parts of the HOL datatype package
    1.12 +  Refinement of parts of the HOL datatype package.
    1.13  
    1.14  * October 2009: Florian Haftmann, TUM
    1.15 -  Generic term styles for term antiquotations
    1.16 +  Generic term styles for term antiquotations.
    1.17  
    1.18  * September 2009: Thomas Sewell, NICTA
    1.19 -  More efficient HOL/record implementation
    1.20 +  More efficient HOL/record implementation.
    1.21  
    1.22  * September 2009: Sascha Boehme, TUM
    1.23 -  SMT method using external SMT solvers
    1.24 +  SMT method using external SMT solvers.
    1.25  
    1.26  * September 2009: Florian Haftmann, TUM
    1.27 -  Refinement of sets and lattices
    1.28 +  Refinement of sets and lattices.
    1.29  
    1.30  * July 2009: Jeremy Avigad and Amine Chaieb
    1.31 -  New number theory
    1.32 +  New number theory.
    1.33  
    1.34  * July 2009: Philipp Meyer, TUM
    1.35 -  HOL/Library/Sum_of_Squares: functionality to call a remote csdp prover
    1.36 +  HOL/Library/Sum_Of_Squares: functionality to call a remote csdp
    1.37 +  prover.
    1.38  
    1.39  * July 2009: Florian Haftmann, TUM
    1.40 -  New quickcheck implementation using new code generator
    1.41 +  New quickcheck implementation using new code generator.
    1.42  
    1.43  * July 2009: Florian Haftmann, TUM
    1.44 -  HOL/Library/FSet: an explicit type of sets; finite sets ready to use for code generation
    1.45 -
    1.46 -* June 2009: Andreas Lochbihler, Uni Karlsruhe
    1.47 -  HOL/Library/Fin_Fun: almost everywhere constant functions
    1.48 +  HOL/Library/FSet: an explicit type of sets; finite sets ready to use
    1.49 +  for code generation.
    1.50  
    1.51  * June 2009: Florian Haftmann, TUM
    1.52 -  HOL/Library/Tree: searchtrees implementing mappings, ready to use for code generation
    1.53 +  HOL/Library/Tree: searchtrees implementing mappings, ready to use
    1.54 +  for code generation.
    1.55  
    1.56  * March 2009: Philipp Meyer, TUM
    1.57 -  minimalization algorithm for results from sledgehammer call
    1.58 +  Minimalization algorithm for results from sledgehammer call.
    1.59 +
    1.60  
    1.61  Contributions to Isabelle2009
    1.62  -----------------------------