Next: The constraints
Up: The scratch area
Previous: The Context-menu
This menu is used to change the presentation of expressions.
- Show all arguments / hide arguments
This is a toggle which says if the system should show or hide the hidden
arguments in an application.
- This is used to hide the first arguments of a functional constant. You are
asked to increment a counter to the number of hidden arguments. You can also
show how to display the constant using other fonts (subscripts, a symbol font,
different font sizes etc).
- Normal Form
Shows the normal form of an object.
- Head Normal Form
Shows the head normal form of an object.
Gives the user a possibility to give a command directly to the proof engine.
It is intended for people who know the commands of the proof engine. It can
be used for bug reports: you type history f to write on file f a
command history of the present state. You can also use it to compute the
normal form of an expression, etc.
- Full view / Restricted view
- Normally, only the type of the constants in the theory is
shown. By selecting a constant and applying this menu, the definitions of the
constant will be shown.
Bj|rn von Sydow
Wed Mar 20 13:05:14 MET 1996