The tree can be used to search for one or more keywords;
the search result acts as a filter.

The strongest point of HLM
is probably the user's ability to attach a custom notation to each definition.
In combination with support for bound variables, many concepts can be displayed
in a familiar way. This notation is even used in the tree, eliminating the need
to remember names. Here is the definition of a generalized sum of natural
numbers:

Instead of typing names
and symbols, the user selects everything from menus. This is the menu for
entering a formula, which includes a list of most-recently used applicable
definitions:

If the needed definition is not in the list of most-recently used items,
clicking on "Operator..." brings up a dialog with an appropriately filtered
tree. Alternatively, one can use drag&drop from the tree on the left.

This is what a
finished definition looks like. If multiple equivalent formulations exist, they
can be entered together, so the library becomes less cluttered and proofs
become shorter. Note that the different definitions for "being prime" are
equivalent only if n>1, which is specified as a
constraint that must be satisfied before the definition can even be used.

Another mathematical feature, special support
for implicit definitions:

Selecting a proof step from the menu inserts it into the proof. Here is the
result of the previous screenshot: