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.

Layout

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.

Command...

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.