Theory CSP

Up to index of Isabelle/HOL/HOL-Complex/CSP

theory CSP
imports CSP_syntax Trace_hide Trace_par Trace_ren Trace_seq CPO_pair CPO_prod CPO_set RS_pair RS_prod
begin

           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2004         |
            |                  July 2005                |
            |                                           |
            |        CSP-Prover on Isabelle2005         |
            |                October 2005  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP = CSP_syntax +
             Trace_hide + Trace_par + Trace_ren + Trace_seq +
             CPO_pair + CPO_prod + CPO_set + RS_pair + RS_prod:

(*****************************************************************

         1. Reusable part of CSP-Prover
         2.
         3. 
         4. 

 *****************************************************************)

end