We use a mouse with three buttons. The left button is used to select a subexpression or a definition. By pressing the shift key it is possible to select more than one definition. This is used when several constants are to be moved simultaneously between the scratch area and the theory window. A double click on the left button opens a text editor on the selected expression. After the text has been edited, it will be parsed and typechecked and will replace the selected expression. The middle button is used to replace a placeholder with an application of a constant. So, first select a placeholder (with the left button) and then move the mouse to the definition of the constant and click on the middle button. A click on the right button will pop up a menu containing all commands which are applicable at the selection. If the selection is a placeholder, then it will also give an approximation of the list of all the applicable constants and locally bound variables. The placeholder will be replaced by a variable by choosing the variable in the list, and it will be replaced by an application of the constant which has been chosen.