This chapter is addressed primarily to those who plan to use Nuprl to build a nontrivial collection of theorems. In it we discuss working with proofs, structuring knowledge in a theory, representing common concepts in the Nuprl logic, and dealing with certain recurring problems.