src/HOL/UNITY/Union.thy
changeset 5259 86d80749453f
parent 5252 1b0f14d11142
child 5313 1861a564d7e2
     1.1 --- a/src/HOL/UNITY/Union.thy	Wed Aug 05 18:21:09 1998 +0200
     1.2 +++ b/src/HOL/UNITY/Union.thy	Wed Aug 05 18:21:37 1998 +0200
     1.3 @@ -12,8 +12,11 @@
     1.4  
     1.5  constdefs
     1.6  
     1.7 -   Join :: "['a program, 'a program] => 'a program"
     1.8 +   Join :: ['a program, 'a program] => 'a program
     1.9      "Join prgF prgG == (|Init = Init prgF Int Init prgG,
    1.10  			 Acts = Acts prgF Un Acts prgG|)"
    1.11  
    1.12 +   Null :: 'a program
    1.13 +    "Null == (|Init = UNIV, Acts = {id}|)"
    1.14 +
    1.15  end