src/HOL/UNITY/Union.thy
changeset 5596 b29d18d8c4d2
parent 5584 aad639e56d4e
child 5611 6957f124ca97
     1.1 --- a/src/HOL/UNITY/Union.thy	Thu Oct 01 18:27:55 1998 +0200
     1.2 +++ b/src/HOL/UNITY/Union.thy	Thu Oct 01 18:28:18 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 -	             Acts0 = UN  i:I. Acts (prg i)|)"
     1.9 +    "JOIN I prg == mk_program (INT i:I. Init (prg i),
    1.10 +			       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 -			 Acts0 = Acts prgF Un Acts prgG|)"
    1.15 +    "Join prgF prgG == mk_program (Init prgF Int Init prgG,
    1.16 +				   Acts prgF Un Acts prgG)"
    1.17  
    1.18     SKIP :: 'a program
    1.19 -    "SKIP == (|Init = UNIV, Acts0 = {}|)"
    1.20 +    "SKIP == mk_program (UNIV, {})"
    1.21  
    1.22  syntax
    1.23    "@JOIN"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3JN _:_./ _)" 10)