1.1 --- a/src/HOL/UNITY/Union.thy	Sat Oct 17 14:43:18 2009 +0200
     1.2 +++ b/src/HOL/UNITY/Union.thy	Mon Feb 08 21:28:27 2010 +0100
     1.3 @@ -36,19 +36,19 @@
     1.4      "safety_prop X == SKIP: X & (\<forall>G. Acts G \<subseteq> UNION X Acts --> G \<in> X)"
     1.5  
     1.6  syntax
     1.7 -  "@JOIN1"     :: "[pttrns, 'b set] => 'b set"         ("(3JN _./ _)" 10)
     1.8 -  "@JOIN"      :: "[pttrn, 'a set, 'b set] => 'b set"  ("(3JN _:_./ _)" 10)
     1.9 +  "_JOIN1"     :: "[pttrns, 'b set] => 'b set"         ("(3JN _./ _)" 10)
    1.10 +  "_JOIN"      :: "[pttrn, 'a set, 'b set] => 'b set"  ("(3JN _:_./ _)" 10)
    1.11  
    1.12  translations
    1.13 -  "JN x : A. B"   == "JOIN A (%x. B)"
    1.14 -  "JN x y. B"   == "JN x. JN y. B"
    1.15 -  "JN x. B"     == "JOIN CONST UNIV (%x. B)"
    1.16 +  "JN x: A. B" == "CONST JOIN A (%x. B)"
    1.17 +  "JN x y. B" == "JN x. JN y. B"
    1.18 +  "JN x. B" == "JOIN CONST UNIV (%x. B)"
    1.19  
    1.20  syntax (xsymbols)
    1.21    SKIP     :: "'a program"                              ("\<bottom>")
    1.22    Join     :: "['a program, 'a program] => 'a program"  (infixl "\<squnion>" 65)
    1.23 -  "@JOIN1" :: "[pttrns, 'b set] => 'b set"              ("(3\<Squnion> _./ _)" 10)
    1.24 -  "@JOIN"  :: "[pttrn, 'a set, 'b set] => 'b set"       ("(3\<Squnion> _\<in>_./ _)" 10)
    1.25 +  "_JOIN1" :: "[pttrns, 'b set] => 'b set"              ("(3\<Squnion> _./ _)" 10)
    1.26 +  "_JOIN"  :: "[pttrn, 'a set, 'b set] => 'b set"       ("(3\<Squnion> _\<in>_./ _)" 10)
    1.27  
    1.28  
    1.29  subsection{*SKIP*}