next up previous contents index
Next: Invoking Transformation Tactics Up: The Proof Editor Previous: Initiating a Refinement

Showing Goals, Subgoals and Rules

 In some circumstances it is convenient to be able to copy goals or subgoals into other proofs. This can't be done directly, but there is a roundabout way. If SEL is pressed while the cursor is in a goal creates a read--only text window containing the text of the goal. The window will be labeled SHOW goal of thmname. The copy mechanism of the text editor can then be used to copy portions of the goal to other windows.

There is a second way to SHOW a goal or subgoal: move the cursor to it and press .

will display the goal or subgoal with all definitions expanded and all terms fully parenthesized. This also works for rules.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995