The files in the directory "book" contain the events that appear in
the book.  For example, the functions defined there do not have
guards.  The directory may be useful for someone who wants to do the
exercises, but does not want to type in the functions presented in the
chapter. In addition, the directory may be useful for someone who
wants to experiment with ACL2 while reading the the book.  

The directory "solutions" contains the solutions to the exercises.
Because adding and proving guards is an implicit exercise, all of the
functions (except for functions used only for proofs) have guards
(which are verified).  Start by reading "solutions/README".