Window inference is a method for contextual rewriting and renement supported by the HOL Window Inference Library. This paper describes a userfriendly interface for window inference. The interface permits the user to select subexpressions by pointing and clicking and to select transformations from menus. The correctness of each transformation step is proved automatically by the HOL system. The interface can be tailored to particular userdened theories. One such extension for program renement is described.