Descriptions A class specification introduces by a list of declarations the “local theory” of a class i.e. a of those entities that may be referenced by their short names in the specification of methods, loops, and commands of the class (the entities introduced in other theories may be always referenced by the long name package.theory.entity). If a class has no such specification, the local theory is empty; the specifications in this class may therefore only refer to entities introduced in other theories.
An import clause from other packages.
Every theory referenced by declarations in the local theory (respectively by the specifications of methods, loops, statements in the current class) must be listed in the clause uses theory, …, either by the long name of the theory or, if the theory was imported, by its short name.
Pragmatics The clause import … is modeled after the semantics of the corresponding Java clause but imports theories rather than classes.
The clause uses theory, … was introduced to simplify the computation of dependencies between classes and theories; in a subsequent version of the language, this clause may be well dropped.