(set-inhibit-output-lst '(proof-tree prove))

(certify-book "bdd-mgr")
:u

(certify-book "bdd-spec")
:u

(certify-book "bdd-prf")
:u