Checking an Istari file (.ist by convention) in batch mode automatically generates an Istari library file (.isto by convention). Istari library files contain constants definitions, lemmas, reductions, and whatever else the user puts into the registry. However, library files do not contain IML code, such as tactics.

Thus Istari content and IML code must be loaded separately:

Library naming conventions

The Istari library adopts a naming convention for the various files that attend an Istari file. We use Nat as an example:

In order to avoid code duplication, most of the code in nat-aux.iml appears in functors, so that can use the code at the appropriate time. (Code that deals with a constant should not be executed until that constant exists.) In nat-load.iml all the functors are called at once, after nat.isto is loaded.