Theory CSP_T_xsymbols

           (*-------------------------------------------*
            |        X symbols for CSP-Prover           |
            |                   June 2008  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_T_xsymbols
imports Domain_T CSP_T_semantics
begin

(*------------------------------------*
 |                                    |
 |             Domain_T               |
 |                                    |
 *------------------------------------*)

notation (xsymbols) memT ("(_/ ∈t _)" [50, 51] 50)
notation (xsymbols) UnionT ("\<Union>t _" [90] 90)
notation (xsymbols) InterT ("\<Inter>t _" [90] 90)

notation (xsymbols) nonmemT ("(_/ ∉t _)" [50, 51] 50)
notation (xsymbols) UnT  ("_ ∪t _" [65,66] 65)
notation (xsymbols) IntT ("_ ∩t _" [70,71] 70)

(*------------------------------------*
 |                                    |
 |           CSP_T_semantics          |
 |                                    |
 *------------------------------------*)

notation (xsymbols) semTf   ("[|_|]Tf")
notation (xsymbols) semTfun ("[|_|]Tfun")

notation (xsymbols) semTfix ("[|_|]Tfix")
notation (xsymbols) semT ("[|_|]T")

notation (xsymbols) refT ("(0_ /\<sqsubseteq>T[_,_] /_)" [51,0,0,50] 50)
notation (xsymbols) refTfix ("(0_ /\<sqsubseteq>T /_)" [51,50] 50)

end