CONTRIBUTORS

 * November 2009: Stefan Berghofer and Lukas Bulwahn, TUM
   A tabled implementation of the reflexive transitive closure.
 
 * November 2009: Lukas Bulwahn, TUM
   Predicate Compiler: a compiler for inductive predicates to
-  equational specfications.
+  equational specifications.
  
 * November 2009: Sascha Boehme, TUM
   HOL-Boogie: an interactive prover back-end for Boogie and VCC.
 
 * October 2009: Jasmin Blanchette, TUM

 * July 2009: Florian Haftmann, TUM
   HOL/Library/FSet: an explicit type of sets; finite sets ready to use
   for code generation.
 
 * June 2009: Florian Haftmann, TUM
-  HOL/Library/Tree: searchtrees implementing mappings, ready to use
+  HOL/Library/Tree: search trees implementing mappings, ready to use
   for code generation.
 
 * March 2009: Philipp Meyer, TUM
-  Minimalization algorithm for results from sledgehammer call.
+  Minimization tool for results from Sledgehammer.
 
 
 Contributions to Isabelle2009
 -----------------------------