Opening, Closing, and Changing Windows

  
Table: Commands For Opening and Closing and Changing Windows

The relevant proof editor commands are shown in Table , and described below. the SELECTSELECT and TRANSFORM commands open up term editor windows. You can edit ML in these windows in the same way you would edit ML in an ML object or in the ML Top Loop .

• Opening a Proof Window
• Closing a Proof Window
• Changing Windows
• Editing The Main Goal
• Editing a Refinement Rule
• Viewing Subgoal Sequents
• Editing a Transformation Tactic