Theory CSP_F_xsymbols

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

theory CSP_F_xsymbols
imports Set_F CSP_F_semantics
begin

(*------------------------------------*
 |                                    |
 |               Set_F                |
 |                                    |
 *------------------------------------*)

notation (xsymbols) memF ("(_/ ∈f _)" [50, 51] 50)
notation (xsymbols) UnionF ("\<Union>f _" [90] 90)
notation (xsymbols) InterF ("\<Inter>f _" [90] 90)

notation (xsymbols) nonmemF  ("(_/ ∉f _)" [50, 51] 50)
notation (xsymbols) UnF      ("_ ∪f _" [65,66] 65)
notation (xsymbols) IntF     ("_ ∩f _" [70,71] 70)

(*------------------------------------*
 |                                    |
 |        CSP_F_semantics             |
 |                                    |
 *------------------------------------*)

notation (xsymbols) semFf   ("[|_|]Ff")
notation (xsymbols) semFfun ("[|_|]Ffun")

notation (xsymbols) semFfix ("[|_|]Ffix")
notation (xsymbols) semF ("[|_|]F")

notation (xsymbols) refF ("(0_ /\<sqsubseteq>F[_,_] /_)" [51,100,100,50] 50)
notation (xsymbols) refFfix ("(0_ /\<sqsubseteq>F /_)" [51,50] 50)

end