Theories

Theories in Russell are containers for all kinds of assertions: Axioms, Definitions, Theorems and of Proofs. Technically theory is a namespace, which helps to avoid the name clash in different theories. For example 'compactness' theorem may mean different things in topology and model theory. Theory is defined with theory keyword:

theory prop_logic {
    ...
}

Theories may be enclosed into each other:

theory A {
    ...
    theory B {
        ...
        theorem X () {
        } 
    }
    ...
}

The reference to an entity in the theory of interest is made with the dot-separated style (from the example above):

thm A.B.X() |- ... ;;