Errata for:
   Jared Davis.   A Self-Verifying Theorem Prover.  PhD thesis, 
   University of Texas at Austin, December 2009.

Page 44.  "This function provides a term level notion of equality, ..."
  should be, "Much like the [equal] function provides a term level notion of equality, ..."

Page 65.  Definition 8.  Subsetp.

   The base case is T, not NIL.
   Thanks to Dan Friedman for spotting the error!

Page 104.  let* is not imported.

Page 161.  Derived Rule 2.  Right Expansion.

   The "given" formula should be "A", not "A \vee B."
   Thanks to Dan Connolly for spotting the error!


Typos spotted by Dan Friedman:

  Pg. 15: "and and" --> "and"
  Pg. 56 and 94: "))" --> ")))" in the basis step
  Pg. 84: "a a" --> "a"
  Pg. 151: Para 2: "then may" --> "then we may"
  

Misc. typos:

  Pg. 446.  "and and" --> "and"
  Pg. 5.    "that theorem prover" --> "that a theorem prover"