src/ZF/UNITY/Union.thy
changeset 35112 ff6f60e6ab85
parent 32960 69916a850301
child 35427 ad039d29e01c
     1.1 --- a/src/ZF/UNITY/Union.thy	Thu Feb 11 22:03:37 2010 +0100
     1.2 +++ b/src/ZF/UNITY/Union.thy	Thu Feb 11 22:06:37 2010 +0100
     1.3 @@ -41,8 +41,8 @@
     1.4        SKIP \<in> X & (\<forall>G \<in> program. Acts(G) \<subseteq> (\<Union>F \<in> X. Acts(F)) --> G \<in> X)"
     1.5    
     1.6  syntax
     1.7 -  "@JOIN1"     :: "[pttrns, i] => i"         ("(3JN _./ _)" 10)
     1.8 -  "@JOIN"      :: "[pttrn, i, i] => i"       ("(3JN _:_./ _)" 10)
     1.9 +  "_JOIN1"     :: "[pttrns, i] => i"         ("(3JN _./ _)" 10)
    1.10 +  "_JOIN"      :: "[pttrn, i, i] => i"       ("(3JN _:_./ _)" 10)
    1.11  
    1.12  translations
    1.13    "JN x:A. B"   == "CONST JOIN(A, (%x. B))"
    1.14 @@ -54,8 +54,8 @@
    1.15    Join  (infixl "\<squnion>" 65)
    1.16  
    1.17  syntax (xsymbols)
    1.18 -  "@JOIN1"  :: "[pttrns, i] => i"     ("(3\<Squnion> _./ _)" 10)
    1.19 -  "@JOIN"   :: "[pttrn, i, i] => i"   ("(3\<Squnion> _ \<in> _./ _)" 10)
    1.20 +  "_JOIN1"  :: "[pttrns, i] => i"     ("(3\<Squnion> _./ _)" 10)
    1.21 +  "_JOIN"   :: "[pttrn, i, i] => i"   ("(3\<Squnion> _ \<in> _./ _)" 10)
    1.22  
    1.23  
    1.24  subsection{*SKIP*}