The ALF libraries provide the user with a collection of theories that may be imported on demand. The libraries contain commonly used sets, functions and properties of these. Two libraries are provided: a very basic one (the Micro Library) containing most commonly used sets; and a more elaborate one (the Contributions Library) where one finds complete developements in ALF.
The libraries are organized in theories where all sets, functions and
properties relating to some concept are defined. In order to use the
constants defined in some theory, one must import the theory. This is
done by using the Import entry in the File menu. ALF then prompts the
user for the name of the theory. The user replies with a theory name,
say N
at. ALF tries to find a file Nat.alf in any of the
directories listed in the environment variable ALFPATH. If this
search is successful, the file is loaded and displayed in the upper
half of the ALF theory window. Imported theories may be used but not
changed or amended. When the user saves her current theory (the
open theory, which is displayed in the lower half of the theory
window), the system records all imported theories and automatically
imports these the next time the current theory is opened. The ALF
libraries reside in subdirectories of a common site-dependent root
directory.
When importing these theories to ALF, applications of some of the
constants are displayed by default with an initial sequence of
arguments suppressed. This is indicated on screen by a vertical arrow
(
) in front of the argument name in the type of the
constant. This is intended to improve readability, but can be changed
using the command Show all arguments in the View menu. Some of the
constants (such as S
igma) are displayed on screen using an
extended font; these cases should be self-explanatory.