src/HOL/UNITY/Union.thy
changeset 5313 1861a564d7e2
parent 5259 86d80749453f
child 5584 aad639e56d4e
     1.1 --- a/src/HOL/UNITY/Union.thy	Thu Aug 13 17:44:50 1998 +0200
     1.2 +++ b/src/HOL/UNITY/Union.thy	Thu Aug 13 18:06:40 1998 +0200
     1.3 @@ -11,6 +11,9 @@
     1.4  Union = SubstAx + FP +
     1.5  
     1.6  constdefs
     1.7 +   JOIN  :: ['a set, 'a => 'b program] => 'b program
     1.8 +    "JOIN I prg == (|Init = INT i:I. Init (prg i),
     1.9 +	           Acts = UN  i:I. Acts (prg i)|)"
    1.10  
    1.11     Join :: ['a program, 'a program] => 'a program
    1.12      "Join prgF prgG == (|Init = Init prgF Int Init prgG,
    1.13 @@ -19,4 +22,10 @@
    1.14     Null :: 'a program
    1.15      "Null == (|Init = UNIV, Acts = {id}|)"
    1.16  
    1.17 +syntax
    1.18 +  "@JOIN"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3JN _:_./ _)" 10)
    1.19 +
    1.20 +translations
    1.21 +  "JN x:A. B"   == "JOIN A (%x. B)"
    1.22 +
    1.23  end