Errata for Computer-Aided Reasoning: ACL2 Case Studies

There are no known errors, yet, but....

See the General Errata for Books About ACL2 and Its Applications for general comments about how the evolution of ACL2 over the years can affect explanations or solution scripts. In particular, as noted there, some solutions may require inclusion of the following two events early in the session.

  (include-book "ordinals/e0-ordinal" :dir :system)
  (set-well-founded-relation e0-ord-<)