next up previous contents
Next: The constraints Up: The scratch area Previous: The Context-menu

The View-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