src/ZF/UNITY/Union.thy
changeset 35427 ad039d29e01c
parent 35112 ff6f60e6ab85
child 45602 2a858377c3d2
     1.1 --- a/src/ZF/UNITY/Union.thy	Tue Mar 02 23:56:13 2010 +0100
     1.2 +++ b/src/ZF/UNITY/Union.thy	Tue Mar 02 23:59:54 2010 +0100
     1.3 @@ -40,23 +40,22 @@
     1.4    "safety_prop(X) == X\<subseteq>program &
     1.5        SKIP \<in> X & (\<forall>G \<in> program. Acts(G) \<subseteq> (\<Union>F \<in> X. Acts(F)) --> G \<in> X)"
     1.6    
     1.7 +notation (xsymbols)
     1.8 +  SKIP  ("\<bottom>") and
     1.9 +  Join  (infixl "\<squnion>" 65)
    1.10 +
    1.11  syntax
    1.12    "_JOIN1"     :: "[pttrns, i] => i"         ("(3JN _./ _)" 10)
    1.13    "_JOIN"      :: "[pttrn, i, i] => i"       ("(3JN _:_./ _)" 10)
    1.14 +syntax (xsymbols)
    1.15 +  "_JOIN1"  :: "[pttrns, i] => i"     ("(3\<Squnion> _./ _)" 10)
    1.16 +  "_JOIN"   :: "[pttrn, i, i] => i"   ("(3\<Squnion> _ \<in> _./ _)" 10)
    1.17  
    1.18  translations
    1.19    "JN x:A. B"   == "CONST JOIN(A, (%x. B))"
    1.20    "JN x y. B"   == "JN x. JN y. B"
    1.21    "JN x. B"     == "CONST JOIN(CONST state,(%x. B))"
    1.22  
    1.23 -notation (xsymbols)
    1.24 -  SKIP  ("\<bottom>") and
    1.25 -  Join  (infixl "\<squnion>" 65)
    1.26 -
    1.27 -syntax (xsymbols)
    1.28 -  "_JOIN1"  :: "[pttrns, i] => i"     ("(3\<Squnion> _./ _)" 10)
    1.29 -  "_JOIN"   :: "[pttrn, i, i] => i"   ("(3\<Squnion> _ \<in> _./ _)" 10)
    1.30 -
    1.31  
    1.32  subsection{*SKIP*}
    1.33