next up previous contents
Next: The Micro Library Up: A user's guide to Previous: The constraints

The ALF Libraries

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.





next up previous contents
Next: The Micro Library Up: A user's guide to Previous: The constraints



Bj|rn von Sydow
Wed Mar 20 13:05:14 MET 1996