next up previous contents
Next: The Goal-menu Up: The scratch area Previous: The Construct-menu

The Edit-menu

Undo
Undo the effects of the last command.
Cut
Replaces the current selection with a placeholder and inserts the selected expression in the cut buffer.
Copy
Copies the current selection into the cut buffer.
Paste
Inserts the content of the cut buffer into the current placeholder.
Clear
Replaces the current expression with a placeholder and deletes all expressions which are consequences of that expression. gif
Edit as Text
Asks the user to input text, which is parsed and replaces the current placeholder.

Unfold
Replace the current selection with its definition (if it is an explicit definition).
Normal Form
Replaces the current selection with its value in normal form.
Head Normal Form
Replaces the current selection with its value in head normal form.
Expand
If the current selection is a definition of an explicitly defined constant then this constant is removed from the scratch area and all occurrences of it is replaced by its definiens. Not implemented yet.

Move to theory
Moves a definition from the scratch area to the theory window.
Move to scratch
Moves a definition from the theory window to the scratch area.



Bj|rn von Sydow
Wed Mar 20 13:05:14 MET 1996