src/HOL/UNITY/Union.thy
changeset 35427 ad039d29e01c
parent 35068 544867142ea4
child 35434 a4babce15c67
     1.1 --- a/src/HOL/UNITY/Union.thy	Tue Mar 02 23:56:13 2010 +0100
     1.2 +++ b/src/HOL/UNITY/Union.thy	Tue Mar 02 23:59:54 2010 +0100
     1.3 @@ -35,21 +35,22 @@
     1.4    safety_prop :: "'a program set => bool"
     1.5      "safety_prop X == SKIP: X & (\<forall>G. Acts G \<subseteq> UNION X Acts --> G \<in> X)"
     1.6  
     1.7 +notation
     1.8 +  SKIP  ("\<bottom>") and
     1.9 +  Join  (infixl "\<squnion>" 65)
    1.10 +
    1.11  syntax
    1.12    "_JOIN1"     :: "[pttrns, 'b set] => 'b set"         ("(3JN _./ _)" 10)
    1.13    "_JOIN"      :: "[pttrn, 'a set, 'b set] => 'b set"  ("(3JN _:_./ _)" 10)
    1.14 +syntax (xsymbols)
    1.15 +  "_JOIN1" :: "[pttrns, 'b set] => 'b set"              ("(3\<Squnion> _./ _)" 10)
    1.16 +  "_JOIN"  :: "[pttrn, 'a set, 'b set] => 'b set"       ("(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 UNIV) (%x. B)"
    1.22  
    1.23 -syntax (xsymbols)
    1.24 -  SKIP     :: "'a program"                              ("\<bottom>")
    1.25 -  Join     :: "['a program, 'a program] => 'a program"  (infixl "\<squnion>" 65)
    1.26 -  "_JOIN1" :: "[pttrns, 'b set] => 'b set"              ("(3\<Squnion> _./ _)" 10)
    1.27 -  "_JOIN"  :: "[pttrn, 'a set, 'b set] => 'b set"       ("(3\<Squnion> _\<in>_./ _)" 10)
    1.28 -
    1.29  
    1.30  subsection{*SKIP*}
    1.31