next up previous contents index
Next: Definitions and Definition Up: The Proof Editor Previous: Showing GoalsSubgoals

Invoking Transformation Tactics

Transformation tactics are tactics which act as proof transformers rather than as generalized refinement rules. To invoke a transformation  tactic, press

( in some older versions). This will bring up a text edit window labelled Transformation Tactic. Type the name of the tactic and any arguments into the window and press ;

will call the tactic and redisplay the proof window to show any effects. If the tactic returns an error message it will be displayed in the command/status window.

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