This research has been done within the ESPRIT Basic Research Action ``Types for Proofs and Programs''. It has been paid by NUTEK and Chalmers.

Note that the type of N is known now, which it was not the previous time we saw the menu.

An unwanted feature of the present version is that the constructors are reordered on the screen by this action. This causes no harm, but is somewhat annoying.

Note that it may be worthwhile to use postscript software to adjust the bounding box.

Contexts consists of list of variable declarations, i.e. a list of variables together with their type. Every constant is defined in a context and the variables in the context can be given a name by using a substitution. This is in an experimental phase and only partly implemented.

Tme implementation of Clear is based on the concept of a local undo; details can be found in [].

Bj|rn von Sydow
Wed Mar 20 13:05:14 MET 1996