Next: The Goal-menu
Up: The scratch area
Previous: The Construct-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.
- 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