Like some other systems, the user communicates with by an interaction loop. The user sends a command to the system. The prover checks it, and sends a response, that can be used by the user to carry on. A sequence of commands can be saved in a file. Such a file can be reevaluated, or compiled. This format is the same for libraries or user's files.
The prover has basically two modes with two sets of commands : the top mode and the proof mode. In the top mode the user can load libraries, describe the theory etc. In the proof mode the user proves a given proposition.
A proof is described by a sequence of commands (called a proof script), always constructed in an interactive way. The proof is constructed top-down : from the goal to ``evidences''. In case the goal is not proved by the command, responses of the system gives subgoals that should be easier than the initial goal. The system gives names for generated hyptothesis or variables. These names make writing easier, but the proof script cannot be understood without the responses of the system.
The system implements essentially the construction of a natural deduction tree in higher order logic, but can be used without really knowing the formal system of natural deduction.
The originality of the system is that the commands can be enhanced by the user, just declaring that some proved formulas of a particular form have to be interpreted as new rules. That allow the system to use few commands. Each command uses more or less automatic reasoning, and a generic automatic command composes the more basics ones.
A module system allows reusing of theories with renaming, eliminating constants and axioms by replacing them with definitions and theorems.
The existing libraries are almost all very basic ones (integers, lists...), but some examples have been developped that are not completly trivial : infinite version of Ramsey theorem, an abstract version of completness of predicate calculus, proof of Zorn lemma ...
In the current version programs extraction is possible but turned off by
default and does not work with all features, see
section A.1.8. Extraction is possible for proofs using
intuitionistic or classical logic. Programs extraction implements
what is described in [1] for intuitionistic functionnal second
order arithmetic, but extended to classical logic and 
-calcul : see [4].