<description>I've moved the exercises out of the book, because I don't feel that I have the time to produce well-tested exercises yet; changed crush's use of autorewrite so that Hint Rewrite commands may be given without explicit hint databases; added a crucial new section to "More Dependent Types"; and added prose and other improvements to "Proof Search by Logic Programming."</description>
</item>
<item>
<item>
<title>A pass through "Proving in the Large"</title>
<title>A pass through "Proving in the Large"</title>