The library contains four kinds of objects: DEF, THM, EVAL and ML. DEF objects define new notations that can be used whenever text is being entered. THM objects contain proofs in the form of proof trees. Each node of the proof tree contains a number of assumptions, a conclusion, a refinement rule and a list of children produced by applying the refinement rule to the assumptions and conclusion. THM objects are checked only when a check command is issued or they are viewed or used as objects from which code is extracted.
EVAL objects contain lists of bindings, where
a binding has the form 
and is terminated by a
double semicolon, `` ;;''.
Checking an EVAL object adds its bindings to the evaluator
environment so that they available to the eval command.
All EVAL objects are checked when they are loaded into the library.
ML objects contain
ML programs, including tactics, which
provide a general way of combining the primitive refinement
rules to form more powerful refinement rules.
Checking an ML object enriches the ML environment.
All ML objects are checked when they are loaded into the library.