src/HOL/UNITY/Union.thy
changeset 5584 aad639e56d4e
parent 5313 1861a564d7e2
child 5596 b29d18d8c4d2
     1.1 --- a/src/HOL/UNITY/Union.thy	Tue Sep 29 15:58:25 1998 +0200
     1.2 +++ b/src/HOL/UNITY/Union.thy	Tue Sep 29 15:58:47 1998 +0200
     1.3 @@ -12,15 +12,15 @@
     1.4  
     1.5  constdefs
     1.6     JOIN  :: ['a set, 'a => 'b program] => 'b program
     1.7 -    "JOIN I prg == (|Init = INT i:I. Init (prg i),
     1.8 -	           Acts = UN  i:I. Acts (prg i)|)"
     1.9 +    "JOIN I prg == (|Init  = INT i:I. Init (prg i),
    1.10 +	             Acts0 = UN  i:I. Acts (prg i)|)"
    1.11  
    1.12     Join :: ['a program, 'a program] => 'a program
    1.13 -    "Join prgF prgG == (|Init = Init prgF Int Init prgG,
    1.14 -			 Acts = Acts prgF Un Acts prgG|)"
    1.15 +    "Join prgF prgG == (|Init  = Init prgF Int Init prgG,
    1.16 +			 Acts0 = Acts prgF Un Acts prgG|)"
    1.17  
    1.18 -   Null :: 'a program
    1.19 -    "Null == (|Init = UNIV, Acts = {id}|)"
    1.20 +   SKIP :: 'a program
    1.21 +    "SKIP == (|Init = UNIV, Acts0 = {}|)"
    1.22  
    1.23  syntax
    1.24    "@JOIN"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3JN _:_./ _)" 10)