Next: The Goal-menu
Up: The scratch area
Previous: The Construct-menu
Undo the effects of the last command.
Replaces the current selection with a placeholder and inserts the selected
expression in the cut buffer.
Copies the current selection into the cut buffer.
Inserts the content of the cut buffer into the current placeholder.
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.
Replace the current selection with its definition (if it is an
- 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.
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