(*-------------------------------------------*
            |           CSP-Prover ver.4.1              |
            |               November 2007               |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

1 Introduction 

This directory contains the theory files for upgrading CSP-Prover
version 4.0 to 4.1. Currently, they are differences from the version
4.0 and need the version 4.0 for making heap files CSP_F_v4_1. Near
future, the theory files for 4.1 will be embedded to proper theory
files in the next CSP-Prover.

The differences from the current stable version (CSP-Prover-4-0) are
summarized as follows:

  o Some laws for sequential compositions etc are added,
  o Tactics are improved for automatising proofs more than ver.4.0,
  o Convenient (conventional) renaming syntax is added like [[a<-b]],
  o Receiving and Sending syntax are kept as much as possible,
    (they are automatically unfold when step-laws are applied to them)
  o Pipe operator is added and the commutative law is proven
  o etc

2 How to use CSP_F.

(note: CSP_F (version 4.0) is required for CSP_F_v4_1)

(1) To build the heap file for CSP_F_v4_1:
    isatool usedir -b CSP_F CSP_F_v4_1

(2) To start Isabelle with CSP_F_v4_1:
    isabelle -I CSP_F_v4_1

(3) To start ProofGeneral with CSP_F_v4_1:
    Isabelle -l CSP_F_v4_1

(4) To use CSP_F_v4_1:
    theory test = CSP_F_v4_1: