The editing facilities of this system were inspired in part by those of the Cornell Program Synthesizer [Teitelbaum & Reps 81] and by AVID [Krafft 81] , the system which first applied these ideas in the setting of proof synthesis. We have been using these editors in the system since 1983. We know how to use them effectively, and while we have not seen demonstrated a better way of generating proofs, based on our experience with these systems we now understand feasible ways to improve them significantly. Research on this topic is under way in our group.