The book, Computer-Aided Reasoning: An Approach, and its companion, Computer-Aided Reasoning: ACL2 Case Studies, were written approximately 20 years ago. From that time to the time of this writing (August, 2019), more than 25 new releases of ACL2 have occurred. Many changes are not reflected in either the hardback or paperback copies or in the specific Errata for the first of these books or the specific Errata for its companion. However, the latest ACL2 documentation is available from the ACL2 home page, and provides up-to-date detailed explanations.
But changes in ACL2 might prevent some of our explanations or solution scripts from replaying in the now-current ACL2. For example, the representation of ordinals has changed and to revert ACL2 to the representation used 20 years ago one must include these two events early in the session.
(include-book "ordinals/e0-ordinal" :dir :system) (set-well-founded-relation e0-ord-<)