The Theorema Session

Mathematical documents containing Theorema code must use one of the Theorema stylesheets,

otherwise the code will not work properly!

This is so because, in addition to styling properties, Theorema stylesheets contain information that influences the evaluation of expressions, in particular the parsing of expressions. Also the appropriate grouping of certain cells is vital for correct interpretation. For these reasons, the Theorema session must be demonstrated in a separate notebook carrying a Theorema style as opposed to Mathematica Tutorial style required for documentation integrated into Mathematica's Help system.

Theorema notebooks are Mathematica notebooks using one of the specific Theorema stylesheets. The stylesheet is always attached as a private style for every notebook, it is not a shared stylesheet. This is so because stylesheets are language- and styling-dependent and they are therfore generated automatically from given templates and attached to the notebook when it is opened or created. Thus, in order to turn certain language- and styling changes into effect, notebooks might need to be re-opened such that the private stylesheets are re-generated.

Every Theorema notebook has an associated directory, in which we store files containing additional information for the notebooks to function properly. An example of such additional information are the proof objects representing the proofs contained in the notebook. These are usually rather big datastructures, and we store them in separate files in order to keep the notebook's size reasonably small.

Theorema Notebooks typically contain dynamic objects, e.g. the environment information for proofs (display of settings when the proof was generated). Mathematica requires a notebook that automatically updates dynamic objects to be stored in a trusted location and maintains a FrontEnd-option TrustedPath. When creating a new Theorema notebook we add the notebook's directory to the TrustedPath (if it is not already there), resulting in a Mathematica warning like

Press "Yes", otherwise Theorema notebooks might show restricted functionality.