src/HOL/UNITY/Union.thy
changeset 5259 86d80749453f
parent 5252 1b0f14d11142
child 5313 1861a564d7e2
equal deleted inserted replaced
5258:d1c0504d6c42 5259:86d80749453f
    10 
    10 
    11 Union = SubstAx + FP +
    11 Union = SubstAx + FP +
    12 
    12 
    13 constdefs
    13 constdefs
    14 
    14 
    15    Join :: "['a program, 'a program] => 'a program"
    15    Join :: ['a program, 'a program] => 'a program
    16     "Join prgF prgG == (|Init = Init prgF Int Init prgG,
    16     "Join prgF prgG == (|Init = Init prgF Int Init prgG,
    17 			 Acts = Acts prgF Un Acts prgG|)"
    17 			 Acts = Acts prgF Un Acts prgG|)"
    18 
    18 
       
    19    Null :: 'a program
       
    20     "Null == (|Init = UNIV, Acts = {id}|)"
       
    21 
    19 end
    22 end