Description A theory definition introduces by a list of declarations a “theory” i.e. a collection of logic entities that may be used in other theories or for the specification of programs.
The clause theory theory states the name of the theory as theory. The optional clause package package states that the new theory resides in package and may be referenced elsewhere by the long name package.theory; likewise any entity this is introduced by declarations may be referenced elsewhere by package.theory.entity. If the package clause is omitted, the theory resides in the unnamed top-level package.
An import clause imports theories from other packages such that they may be referenced from the current theory not only by their long names of form package.theory by also by their short names of form theory. A clause
import package.*;
imports all theories from package; a clause
import package.theory;
imports from package only theory. If multiple package.* import theories with the same name, these theories can be only referenced by their long name unless one of the packages is also imported as package.theory; then this theory can also be referenced by the short name. Multiple package.theory imports of different theories with the same short name theory are prohibited.
Every theory referenced by declarations in the current theory 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 A theory with long name package.theory must reside in a file with name theory.theory in a subdirectory package of a directory that is considered as a root of the package hierarchy. The name package may have form p1.p2.…pn; the corresponding directory path is then p1/p2/…/pn.
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.