************************** IMPORTANT **********************************
These books can be certified in ACL2 versions 2.4 and 2.5.
Due to a bug in version 2.5, a useful meta rule in multiset.lisp is not
applied where needed in the examples mccarthy-91.lisp and
ackermann.lisp (there is no such problem in version 2.4).
To fix this problem in version 2.5, the file patch-meta.lisp has to be
used. Thanks to Matt Kaufmann for sending us the patch (it will be
included in version 2.6)

If you certify these books using make, you don't have to worry about
that, because the patch is loaded anyway. If you certify the files
individually, you have to load the patch before the certification
process. 
************************************************************************