%%%%%%%%%%%%%%%%%%%%%%%%%%%
% UTP ProofPower Theories %
%%%%%%%%%%%%%%%%%%%%%%%%%%%

- This is the source code of the ProofPower theories that
implement the UTP theories of relations, designs, reactive
predicates, CSP processes and the theory of Circus.

- You MUST have ProofPower already installed in your machine in
order to load these definitions.

- To load these theories:

    1. Make the files load-theories and clear-all executables,
    using the following unix commands
        chmod +x load-*
        chmod +x clear-theories

    2. Execute the following lines of command (within the directory
    pp-theories-source)
        pp_make_database -f -p zed ./db/circus
        chmod +w ./db/circus.polydb

    3. Load the theories:
        - Execute the file
            ./load-z-library
        - After ProofPower finishes loading the theory,
        save it by executing the following command in ProofPower-Z
            save();

        - Execute the file
            ./load-relations
        - After ProofPower finishes loading the theory,
        save it by executing the following command in ProofPower-Z
            save();

        - Execute the file
            ./load-okay
        - After ProofPower finishes loading the theory,
        save it by executing the following command in ProofPower-Z
            save();

        - Execute the file
            ./load-designs
        - After ProofPower finishes loading the theory,
        save it by executing the following command in ProofPower-Z
            save();

        - Execute the file
            ./load-wtr
        - After ProofPower finishes loading the theory,
        save it by executing the following command in ProofPower-Z
            save();

        - Execute the file
            ./load-reactive
        - After ProofPower finishes loading the theory,
        save it by executing the following command in ProofPower-Z
            save();

        - Execute the file
            ./load-csp
        - After ProofPower finishes loading the theory,
        save it by executing the following command in ProofPower-Z
            save();

        - Execute the file
            ./load-circus
        - After ProofPower finishes loading the theory,
        save it by executing the following command in ProofPower-Z
            save();

    3. Execute the file clear-theories in order to organise the files in
    the file structure.
