Synched up doc.lisp
fix for acl2(r) build