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

(certify-book "records")
:u

(certify-book "cdeq-defs")
:u

(certify-book "cdeq-phase1")
:u

(certify-book "cdeq-phase2")
:u

(certify-book "cdeq-phase3")
:u

(certify-book "cdeq-phase4")
:u