The revapp-prp.lisp files tries to include the rev-prp book, but the include fails on the excuse that rev-prp is not compiled. Usually, I've found this to mean that the (in-package "ACL2") directive is missing, but in this case, it's not, and everything in the rev-prp book admits. I don't see a way to include files with bug rpts, but the files are at the moment here:
http://www.cs.ou.edu/~rlpage/caleb/incl-bk-bug.zip
The revapp-prp.lisp files tries to include the rev-prp book, but the include fails on the excuse that rev-prp is not compiled. Usually, I've found this to mean that the (in-package "ACL2") directive is missing, but in this case, it's not, and everything in the rev-prp book admits. I don't see a way to include files with bug rpts, but the files are at the moment here: http://www.cs.ou.edu/~rlpage/caleb/incl-bk-bug.zip