The Nuprl system has been designed to accommodate the top--down construction of proofs by refinement. In this style one proves a judgement (i.e., a goal) by applying a refinement rule, thereby obtaining a set of judgements called subgoals, and then proving each of the subgoals. The mechanics of using the proof--editing system were discussed in chapter 7. In this section we will describe the refinement rules themselves. First we give some general comments regarding the rules and then proceed to give a description of each rule.